fact: Fixpoint MTele_val {s} {n : MTele} : MTele_Sort s n -> s := match n as n return MTele_Sort s n -> s with | mBase => fun f => f | mTele F => fun f => ForAll (fun x => MTele_val (f x)) end.
imports: Mtac2(Sorts Specif)