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.Type.Loader Equations.Type.Logic Equations.Type.FunctionalExtensionality Equations.Type.WellFounded Equations.Type.DepElim Equations.Type.Subterm Equations.Type.Tactics Equations.Type.FunctionalInduction