fact: Fixpoint MTele_sort {s : Sort} {n : MTele} : forall S : MTele_Sort s n, Type := match n return MTele_Sort s n -> _ with | mBase => fun S => selem_of S | mTele F => fun S => forall x, MTele_sort (S x) end.
imports: Mtac2(Sorts Specif)