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.HoTT.Loader Equations.HoTT.Logic Equations.HoTT.WellFounded Equations.HoTT.DepElim Equations.HoTT.Tactics Equations.HoTT.FunctionalInduction Equations.HoTT.Subterm HoTT(Basics.Tactics)