fact: Fixpoint flatten_forall_unapply {t : Telescope} : forall {P : flattenT_sig t -> Type}, (forall x : flattenT_sig t, P x) -> flatten_forall (flattenT_unapply P) := match t return forall {P : flattenT_sig t -> Type}, (forall x : flattenT_sig t, P x) -> flatten_forall (flattenT_unapply P) with | bottom => fun X x => x tt | tele A B => fun P f x => @flatten_forall_unapply (B x) _ (fun x' => f _) end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Relations.Relation_Definitions Coq.Classes.Morphisms