fact: Fixpoint curry {m : MTele} : forall {T : MTele_Ty m}, (forall U : ArgsOf m, M (apply_sort T U)) -> MFA T := match m with | mBase => fun T F => F tt | mTele f => fun T F x => curry (fun U => F (mexistT _ x U)) end.
imports: Mtac2(Base Specif MTele)