fact: Definition ForAll {sort : Sort} {A : Type} : (A -> stype_of sort) -> stype_of sort := match sort as sort' return ((A -> stype_of sort') -> stype_of sort') with | Propₛ => fun F => forall a : A, F a | Typeₛ => fun F => forall a : A, F a end.