fact: Fixpoint flattenT_unapply_apply {t : Telescope} {X : Type} {struct t} : forall (f : flattenT t X), flattenT_eq f (flattenT_unapply (flattenT_apply f)) := match t return forall (f : flattenT t X), flattenT_eq f (flattenT_unapply (flattenT_apply f)) with | bottom => fun f => eq_refl | tele A B => fun f x => @flattenT_unapply_apply (B x) X (f x) 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