funext : ∀ {A : Type} {B : A → Type} {f g : Π (a : A), B a}, (∀ (a : A), f a = g a) → f = g
strong_indefinite_description : Π {A : Type} (P : A → Prop), nonempty A → { (x : A) | (∃ (x : A), P x) → P x }