fact: Definition tele_fix_functional_type := tele_forall_uncurry T (fun x => ((tele_forall_uncurry@{i k k} T (fun y => R y x -> tele_type_app T P y))) -> tele_type_app T P x).
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)