Require MinMJ_Occurs.

(* Support functions for phibar. *)
(*
Recursive Definition
    MssubstVMV2 : V->M->V->V->Ms->M :=
	x m i j ms => 
		(Setifb M 
			(nateqb i j)
			(sc x (mcons m ms))
			(sc (drop_V i j) ms)).

Fixpoint
    MsubstVMV1 [m:M] : V->M->V->M :=
	[x:V][m':M][i:nat]<M>Case m of
	    (* x;ms *)[z:V][ms:Ms]
		(MssubstVMV2 x m' i z (MssubstVMV1 ms x m' i))
	    (* lambda m *)[m'':M]
		(lambda (MsubstVMV1 m'' (lift_V O x) (lift_M O m') (S i)))
end with
    MssubstVMV1 [ms:Ms] : V->M->V->Ms :=
	[x:V][m:M][i:nat]<Ms>Case ms of
	    (* mnil *)
		mnil
	(* m::ms *)[m':M][ms':Ms]
		(mcons (MsubstVMV1 m' x m i) (MssubstVMV1 ms' x m i))
end.
*)

Fixpoint MsubstVMV1 [m:M] : V->M->V->M :=
	[x:V][m':M][i:V]<M>Case m of
	[z:V][ms:Ms]
	 (Setifb M (nateqb i z) (sc x (mcons m' (MssubstVMV1 ms x m' z)))
				(sc (drop_V i z) (MssubstVMV1 ms x m' i)))
	[m'':M]
	 (lambda (MsubstVMV1 m'' (lift_V O x) (lift_M O m') (S i)))
end with
MssubstVMV1 [ms:Ms] : V->M->V->Ms :=
	[x:V][m':M][i:V]<Ms>Case ms of
	mnil
	[m'':M][ms':Ms]
	 (mcons (MsubstVMV1 m'' x m' i) (MssubstVMV1 ms' x m' i))
end.

Recursive Definition
    MsubstVMV : V->M->V->M->M :=
	x m i m' => (MsubstVMV1 m' x m i).

Recursive Definition
    MssubstVMV : V->M->V->Ms->Ms :=
	x m i ms => (MssubstVMV1 ms x m i).

Lemma Drop_Lift_V :
	(x:V)(i:nat)
	 (drop_V i (lift_V i x))=x.

Definition drop_lift_m : M->Prop :=
	[m:M](i:nat)(drop_M i (lift_M i m))=m.

Definition drop_lift_ms : Ms->Prop :=
	[ms:Ms](i:nat)(drop_Ms i (lift_Ms i ms))=ms.

Lemma drop_lift_M : 
	((m:M)(drop_lift_m m))/\((ms:Ms)(drop_lift_ms ms)).

Lemma Drop_Lift_M : (i:nat)(m:M)(drop_M i (lift_M i m))=m.

Lemma Drop_Lift_Ms : (i:nat)(ms:Ms)(drop_Ms i (lift_Ms i ms))=ms.

Lemma MSVMV1 :
	(x:V)(m:M)(y,z:V)(ms:Ms)
	  (MsubstVMV x m y (sc z ms)) =
	   (Setifb M
		   (nateqb y z)
		   (sc x (mcons m (MssubstVMV x m z ms)))
		   (sc (drop_V y z) (MssubstVMV x m y ms))).

Lemma MSVMV2 : (x:V)(m:M)(m':M)(y:V)
		(MsubstVMV x m y (lambda m')) =
		 (lambda (MsubstVMV (lift_V O x) (lift_M O m) (S y) m')).

Lemma MSVMV3 : (x:V)(m:M)(y:V)((MssubstVMV x m y mnil) = mnil).

Lemma MSVMV4 : (x:V)(m:M)(y:V)(m':M)(ms:Ms)
		((MssubstVMV x m y (mcons m' ms)) =
		 (mcons (MsubstVMV x m y m')
			(MssubstVMV x m y ms))).

Lemma Lift_Drop_V :
	(x:V)(i:nat)
	 ~(Occurs_In_V i x)->
	  (lift_V i (drop_V i x))=x.

Definition lift_drop_m : M->Prop :=
	[m:M](i:nat)
	 ~(Occurs_In_M i m)->
	  (lift_M i (drop_M i m))=m.

Definition lift_drop_ms : Ms->Prop :=
	[ms:Ms](i:nat)
	 ~(Occurs_In_Ms i ms)->
	  (lift_Ms i (drop_Ms i ms))=ms.

Lemma lift_drop_M : 
	((m:M)(lift_drop_m m))/\((ms:Ms)(lift_drop_ms ms)).

Lemma Lift_Drop_M :
	(i:nat)(m:M)
	 ~(Occurs_In_M i m)->
	  (lift_M i (drop_M i m))=m.

Lemma Lift_Drop_Ms :
	(i:nat)(ms:Ms)
	 ~(Occurs_In_Ms i ms)->
	  (lift_Ms i (drop_Ms i ms))=ms.