fact: Fixpoint MTele_const {s : Sort} {T : s} {n : MTele} : @MTele_Const s T n -> stype_of s := match n return MTele_Const T n -> _ with | mBase => fun _ => T | mTele F => fun C => ForAll (fun x => MTele_const (App C x)) end.
imports: Mtac2(Sorts Specif)