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