Require MinMJ_LJ.
Require MinMJ_MJ.
Require MinMJ_NJ.
Require MinMJ_Occurs_Lift.

Recursive Definition
    Hyps_Exchange : nat->Hyps->Hyps :=
	i MT => MT |
	i (Add_Hyp P MT) => (Add_Hyp P MT) |
	O (Add_Hyp P (Add_Hyp Q h)) =>
		(Add_Hyp Q (Add_Hyp P h)) |
	(S i) (Add_Hyp P (Add_Hyp Q h)) =>
		(Add_Hyp P (Hyps_Exchange i (Add_Hyp Q h))).

Recursive Definition
    V_Exchange : nat->V->V :=
	i j => (Setifb V
		       (nateqb i j)
		       (S i)
		       (Setifb V
			       (nateqb (S i) j)
			       i
			       j)).

Recursive Definition
    L_Exchange : nat->L->L :=
	i (vr x) => (vr (V_Exchange i x)) |
	i (app x l1 l2) =>
		(app (V_Exchange i x)
		     (L_Exchange i l1)
		     (L_Exchange (S i) l2)) |
	i (lm l) => (lm (L_Exchange (S i) l)).

Fixpoint
    M_Exchange1 [m:M] : nat->M :=
	[i:nat]<M>Case m of
	    (* x;ms *)[x:V][ms:Ms]
		(sc (V_Exchange i x) (Ms_Exchange1 ms i))
	    (* lam m *)[m':M]
		(lambda (M_Exchange1 m' (S i)))
end with
    Ms_Exchange1 [ms:Ms] : nat->Ms :=
	[i:nat]<Ms>Case ms of
	    (* mnil *)
		mnil
	    (* m::ms *)[m:M][ms':Ms]
		(mcons (M_Exchange1 m i) (Ms_Exchange1 ms' i))
end.

Recursive Definition
    M_Exchange : nat->M->M :=
	i m => (M_Exchange1 m i).

Recursive Definition
    Ms_Exchange : nat->Ms->Ms :=
	i ms => (Ms_Exchange1 ms i).

Fixpoint
    N_Exchange1 [n:N] : nat->N :=
	[i:nat]<N>Case n of
	    (* lam n *)[n':N]
		(lam (N_Exchange1 n' (S i)))
	    (* an a *)[a:A]
		(an (A_Exchange1 a i))
end with
    A_Exchange1 [a:A] : nat->A :=
	[i:nat]<A>Case a of
	    (* ap a n *)[a':A][n:N]
		(ap (A_Exchange1 a' i) (N_Exchange1 n i))
	    (* var x *)[x:V]
		(var (V_Exchange i x))
end.

Recursive Definition N_Exchange : nat->N->N :=
i n => (N_Exchange1 n i).

Recursive Definition A_Exchange : nat->A->A :=
i a => (A_Exchange1 a i).

Lemma MExch1 : (i:nat)(x:V)(ms:Ms)
	((M_Exchange i (sc x ms)) =
	 (sc (V_Exchange i x) (Ms_Exchange i ms))).

Lemma MExch2 : (i:nat)(m:M)((M_Exchange i (lambda m)) = (lambda (M_Exchange (S i) m))).

Lemma MExch3 : (i:nat)(Ms_Exchange i mnil)=mnil.

Lemma MExch4 : (i:nat)(m:M)(ms:Ms)((Ms_Exchange i (mcons m ms)) = 
			    (mcons (M_Exchange i m) (Ms_Exchange i ms))).

Lemma NExch1 : (i:nat)(n:N)((N_Exchange i (lam n)) = (lam (N_Exchange (S i) n))).

Lemma NExch2 : (i:nat)(a:A)((N_Exchange i (an a)) = (an (A_Exchange i a))).

Lemma NExch3 : (i:nat)(a:A)(n:N)
	((A_Exchange i (ap a n)) = (ap (A_Exchange i a) (N_Exchange i n))).

Lemma NExch4 : (i:nat)(x:V)((A_Exchange i (var x)) = (var (V_Exchange i x))).