proposition: Lemma tele_forall_pack_unpack (T : tele) (P : T -> Type) (f : forall t, P t) : forall x, tele_forall_pack T P (tele_forall_unpack T P f) x = f x.
proof: Proof. induction T; simpl. reflexivity. intros [a b]. simpl. apply (X a (fun b => P (a, b))). 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