proposition: Lemma tele_forall_app_type (T : tele@{i}) (P : tele_type T) (f : forall t, tele_type_app T P t) : forall x, tele_forall_app T P (tele_forall_type_app T P f) x = f x.
proof: Proof. induction T; simpl. - reflexivity. - cbn. intros [a b]. simpl. apply X. Defined.
imports: Equations.HoTT.Loader Equations.HoTT.Logic Equations.HoTT.WellFounded Equations.HoTT.DepElim Equations.HoTT.Tactics Equations.HoTT.FunctionalInduction Equations.HoTT.Subterm HoTT(Basics.Tactics)