proposition: Lemma tele_fix : tele_forall T P.
proof: Proof. refine (tele_forall_type_app _ _ (@Subterm.FixWf (tele_sigma T) _ wf (tele_type_app T P) (fun x H => tele_forall_pack T _ fn x (tele_forall_unpack T _ H)))). Defined.
imports: Equations.Prop.Loader Coq(FunctionalExtensionality) Equations.Prop.DepElim Equations.Prop.Tactics Equations.Prop.FunctionalInduction