fact: Fixpoint apply_ConstMap {si so : Sort} {n : MTele} {T : si} {G : T -> so} : forall {C : MTele_Const T n} (v : MTele_val (MTele_ConstMap so G C)), forall a : ArgsOf n, G (apply_const C a) := match n with | mBase => fun T v a => v | mTele F => fun T v '(mexistT _ x a) => apply_ConstMap (App v x) a end.
imports: Mtac2(Sorts Specif)