fact: Definition MTele_ConstMap {si : Sort} (so : Sort) {n : MTele} {T : si} (G : T -> so) : forall (C : MTele_Const T n), MTele_Sort so n := fun C => curry_sort so (fun a => G (apply_const C a)).
imports: Mtac2(Sorts Specif)