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