Require MinMJ_Occurs.

(* Support functions for phibar. *)

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.

(Unfold V; Intros n i; Cut (nat_compare2 i n); Auto; Unfold lift_V;
 Unfold nat_compare2; Intros c; Case c; Clear  c; Intros).
(Rewrite -> ltb_is_lt3; Simpl; Unfold drop_V).
(Rewrite -> ltb_is_lt3; Auto).

(Apply ltnotlt; Auto).

(Case H; Clear  H; Intros).
(Rewrite -> ltb_is_lt3; Auto; Simpl; Unfold drop_V;
 Rewrite -> ltb_is_lt3; Auto).

(Rewrite -> ltb_is_lt1; Auto; Simpl; Unfold drop_V;
 Rewrite -> ltb_is_lt1; Auto).
Save.

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)).

Apply M_Ms_ind.
(Unfold drop_lift_ms;Unfold drop_lift_m ).
Intros.
Rewrite -> LIFTM1.
Rewrite -> DROPM1.
Rewrite -> H.
Auto.
Rewrite -> Drop_Lift_V.
Auto.

Unfold drop_lift_m .
Intros.
Simpl.
Rewrite -> H.
Auto.

Unfold drop_lift_ms .
Auto.

Unfold drop_lift_m .
Unfold drop_lift_ms .
Intros.
Rewrite -> LIFTM4.
Rewrite -> DROPM4.
(Rewrite -> H;Rewrite -> H0).
Auto.
Save.

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

Cut ((m:M)(drop_lift_m m))/\((ms:Ms)(drop_lift_ms ms)).
Unfold drop_lift_m.
Intros H.
Case H.
Auto.
Exact drop_lift_M.
Save.

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

Cut ((m:M)(drop_lift_m m))/\((ms:Ms)(drop_lift_ms ms)).
Unfold drop_lift_ms.
Intros H.
Case H.
Auto.
Exact drop_lift_M.
Save.

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))).

Auto.
Save.

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')).
Auto.
Save.

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

Auto.
Save.

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))).

Auto.
Save.

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

(Intros;
 Cut (nat_compare2 i x);
 [ Destruct 1; [ Intro | Destruct 1; Intro ] | Auto ]; Unfold drop_V).
(Rewrite -> ltb_is_lt3; Auto; Simpl; Unfold lift_V).
(Rewrite -> ltb_is_lt3; Auto).
(Inversion_clear H1; Auto).

(Apply lt_not_ltpred; Auto).

Auto_Contra H.

(Rewrite -> ltb_is_lt1; Auto; Unfold Setifb; Unfold lift_V;
 Rewrite -> ltb_is_lt1; Auto).
Save.

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)).

(Apply M_Ms_ind; Unfold lift_drop_m; Unfold lift_drop_ms; Auto; Intros).
(Rewrite -> DROPM1; Rewrite -> LIFTM1; Rewrite -> H; Auto).
(Rewrite -> Lift_Drop_V; Auto).
(Unfold not; Intros; Apply H0; Auto).

(Unfold not; Intros; Apply H0; Auto).

(Rewrite -> DROPM2; Rewrite -> LIFTM2; Rewrite -> H; Auto).
(Unfold not; Intros; Apply H0; Auto).

(Rewrite -> DROPM4; Rewrite -> LIFTM4; Rewrite -> H; Auto).
(Rewrite -> H0; Auto).
(Unfold not; Intros; Apply H1; Auto).

(Unfold not; Intros; Apply H1; Auto).
Save.

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

Cut ((m:M)(lift_drop_m m))/\((ms:Ms)(lift_drop_ms ms)).
(Unfold lift_drop_m; Intros c; Case c; Auto).

Exact lift_drop_M.
Save.

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

Cut ((m:M)(lift_drop_m m))/\((ms:Ms)(lift_drop_ms ms)).
(Unfold lift_drop_ms; Intros c; Case c; Auto).

Exact lift_drop_M.
Save.