proposition: Lemma flatten_forall_apply_of_unapply_eq {t X} f x : eq_rect _ (fun T : Type => T) (flatten_forall_apply f x) _ (eq_sym (flattenT_apply_unapply (fun _ => X) _)) = @flatten_forall_apply_of_unapply t X f x.
proof: Proof. induction t as [|A B IHt]; simpl in *. { destruct x; simpl; reflexivity. } { specialize (IHt (projT1 x) (f (projT1 x)) (projT2 x)). etransitivity; [ clear IHt | exact IHt ]. repeat apply f_equal. etransitivity; [ | apply concat_1p ]. apply f_equal2; [ | reflexivity ]. apply ap_const. } Defined.
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