fact: Fixpoint curry_val {s : Sort} {m : MTele} : forall {T : MTele_Sort s m}, (forall a: ArgsOf m, apply_sort T a) -> MTele_val T := match m with | mBase => fun T f => f tt | mTele F => fun T f => Fun (fun x => curry_val (fun a => f (mexistT _ _ _))) end.
imports: Mtac2(Sorts Specif)