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. rewrite H. reflexivity. Defined.
imports: Equations.Prop.Loader Coq(FunctionalExtensionality) Equations.Prop.DepElim Equations.Prop.Tactics Equations.Prop.FunctionalInduction