fact: Fixpoint flatten_forall_eq_rect_flattenT_unapply_Proper {t} : forall {P Q : flattenT_sig t -> Type} (H : forall x, P x = Q x) (f : forall x, P x), flatten_forall_eq (flatten_forall_eq_rect (@flattenT_unapply_Proper t _ P (fun x => Q x) H) (flatten_forall_unapply f)) (flatten_forall_unapply (fun x => eq_rect _ (fun P => P) (f x) _ (H x))) := match t return forall {P Q : flattenT_sig t -> Type} (H : forall x, P x = Q x) (f : forall x, P x), flatten_forall_eq (flatten_forall_eq_rect (@flattenT_unapply_Proper t _ P (fun x => Q x) H) (flatten_forall_unapply f)) (flatten_forall_unapply (fun x => eq_rect _ (fun P => P) (f x) _ (H x))) with | bottom => fun P Q H k => eq_refl | tele A B => fun P Q H f a => @flatten_forall_eq_rect_flattenT_unapply_Proper (B a) _ _ _ _ end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Classes.Morphisms Fiat.Common.Equality Fiat.Common.Telescope.Core Fiat.Common.Telescope.Instances