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