fact: Fixpoint flattenT_apply_unapply {t : Telescope} {X : Type} {struct t} : forall (f : flattenT_sig t -> X) (x : flattenT_sig t), f x = flattenT_apply (flattenT_unapply f) x := match t return forall (f : flattenT_sig t -> X) (x : flattenT_sig t), f x = flattenT_apply (flattenT_unapply f) x with | bottom => fun f x => match x with | tt => eq_refl end | tele A B => fun f x => eq_trans (f_equal f match x return x = existT (fun a => flattenT_sig (B a)) (projT1 x) (projT2 x) with | existT _ _ => eq_refl end) (@flattenT_apply_unapply (B (projT1 x)) X (fun p => f (existT (fun x' => flattenT_sig (B x')) (projT1 x) p)) (projT2 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