fact: Fixpoint flatten_forall_eq_rect_symmetry_flattenT_unapply_apply {t} : forall {f k}, flatten_forall_eq (flatten_forall_eq_rect (symmetry (@flattenT_unapply_apply t Type f)) (flatten_forall_unapply (flatten_forall_apply k))) k := match t return forall {f k}, flatten_forall_eq (flatten_forall_eq_rect (symmetry (@flattenT_unapply_apply t Type f)) (flatten_forall_unapply (flatten_forall_apply k))) k with | bottom => fun f k => eq_refl | tele A'' B'' => fun f k a => @flatten_forall_eq_rect_symmetry_flattenT_unapply_apply (B'' a) (f a) (k 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