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