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