fmod META-SUBSTITUTION is

protecting QID .
protecting NAT .
protecting PROP .
protecting ABSTRACT-SYNTAX .

var i j k n m : Nat .
var X Y Z X' Y' Z' : Qid .
var K K1 K2 : Const .
var U U1 U2 : Univ .
var A B M N P Q R : Trm .
var TN TM TTM T TT T' TT' T1 TT1 T2 TT2 T3 TT3 T1' T2' T3' : Trm .
var MV MV' : MetaVar .
var CE CE' : CtxtEl .
var CL C C' C1 C2 : Ctxt .
var SE SE' : SubstEl .
var S S' S1 S2 S3 S4 S5 S6 : Subst .
var I J : Qid .
var PI : Pi .
var UNV : Unv .
var ABS : Abs .
var DEF : Def .

var CM : ClosedTrm .
var CC : ClosedCtxt .
var CCE : ClosedCtxtEl .

--- Metavariable Substitution (Textual)

op  <_:=_>_ : MetaVar Trm Trm -> Trm [prec 59 gather (& & &)] .
op  <_:=_>_ : MetaVar Trm Ctxt -> Ctxt [prec 59 gather (& & &)] .
op  <_:=_>_ : MetaVar Trm CtxtEl -> CtxtEl [prec 59 gather (& & &)] .
op  <_:=_>_ : MetaVar Trm Subst -> Subst [prec 59 gather (& & &)] .

eq  < MV := Q > CM = CM .
eq  < MV := Q > CC = CC .
eq  < MV := Q > CCE = CCE .

eq  < MV := Q > [X : T] = [X : < MV := Q > T] .
eq  < MV := Q > [X | T] = [X | < MV := Q > T] .
eq  < MV := Q > {X : T} = {X : < MV := Q > T} .
eq  < MV := Q > {X | T} = {X | < MV := Q > T} .
eq  < MV := Q > [X := M] = [X := < MV := Q > M] .
eq  < MV := Q > {X := M} = {X := < MV := Q > M} .
eq  < MV := Q > {{X : T1 : T2}} = {{X : < MV := Q > T1 : < MV := Q > T2}} .

eq  < MV := Q > emptySubst = emptySubst .
eq  < MV := Q > (X := M) = (X := < MV := Q > M) .
eq  < MV := Q > (shift X) = (shift X) .
eq  < MV := Q > (lift X S) = (lift X (< MV := Q > S)) .

eq  < MV := Q > emptyCtxt = emptyCtxt .
eq  < MV := Q > (C CE) = (< MV := Q > C) (< MV := Q > CE) .

eq  < MV := Q > K = K .

eq  < MV := Q > X{m} = X{m} .

eq  < MV := Q > (M N) = ((< MV := Q > M) (< MV := Q > N)) . 
eq  < MV := Q > (M | N) = ((< MV := Q > M) | (< MV := Q > N)) . 
eq  < MV := Q > (M :: N) = ((< MV := Q > M) :: (< MV := Q > N)) . 
eq  < MV := Q > (MAX T1 T2) = (MAX (< MV := Q > T1) (< MV := Q > T2)) . 

eq  < MV := Q > (ABS M) = (< MV := Q > ABS) (< MV := Q > M) .
eq  < MV := Q > (PI M) = (< MV := Q > PI) (< MV := Q > M) .
eq  < MV := Q > (DEF M) = (< MV := Q > DEF) (< MV := Q > M) .
eq  < MV := Q > (UNV M) = (< MV := Q > UNV) (< MV := Q > M) .
eq  < MV := Q > (S * M) = (< MV := Q > S) * (< MV := Q > M) .
eq  < MV := Q > (S1 * S2) = (< MV := Q > S1) * (< MV := Q > S2) .

ceq < MV := Q > MV = Q if MV =/= ? .
ceq < MV := Q > MV' = MV' if MV =/= MV' .

endfm