fact: Fixpoint MTele_to {s : Sort} {B : s} {G: forall X, (X -> s) -> s} {n : MTele} (b : B) (g : forall X F, G X F) : MTele_To B G n := match n as n return MTele_To B G n with | mBase => b | mTele F => g _ _ end.
imports: Mtac2(Sorts Specif)