fact: Fixpoint MTele_ConstSort {s : Sort} {n : MTele} : forall {T : s} (C : MTele_Const T n), MTele_Sort s n := match n with | mBase => fun T _ => T | mTele F => fun _ C t => MTele_ConstSort (App C t) end.
imports: Mtac2(Sorts Specif)