fact: Fixpoint MTele_open (M : Type -> Prop) {X : Type -> Prop} {m}: forall (T : MTele_Ty m), (forall R, MT_Acc R T -> X R) -> MTele_ty X T := match m as m' return forall T : MTele_Ty m', (forall R, MT_Acc R T -> X R) -> MTele_ty X T with | mBase => fun T b => b _ (fun X x => x) | mTele F => fun T b x => MTele_open M (T x) (fun R f => b R (fun M' mR => f M' (mR x))) end.
imports: Mtac2(Sorts Specif)