fact: Fixpoint flatten_forall_eq_rect {t : Telescope} : forall {P Q : flattenT t Type}, flattenT_eq P Q -> flatten_forall P -> flatten_forall Q := match t return forall {P Q : flattenT t Type}, flattenT_eq P Q -> flatten_forall P -> flatten_forall Q with | bottom => fun P Q H k => eq_rect _ (fun x => x) k _ H | tele A B => fun P Q H k a => @flatten_forall_eq_rect (B a) (P a) (Q a) (H a) (k a) end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Relations.Relation_Definitions Coq.Classes.Morphisms