3 lines
262 B
Text
3 lines
262 B
Text
quot.sound : ∀ {α : Type u} [s : setoid α] {a b : α}, a ≈ b → ⟦a⟧ = ⟦b⟧
|
||
classical.strong_indefinite_description : Π {a : Type u} (p : a → Prop), nonempty a → {x // (∃ (y : a), p y) → p x}
|
||
propext : ∀ {a b : Prop}, (a ↔ b) → a = b
|