Require MinMJ_LMN.

Recursive Definition drop_V : nat->V->V :=
j i => (Setifb V (ltb i j) i (pred i)).

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

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

Recursive Definition
    drop_M : nat->M->M :=
	i m => (drop_M1 m i).

Recursive Definition
    drop_Ms : nat->Ms->Ms :=
	i ms => (drop_Ms1 ms i).

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

Recursive Definition
    drop_N : nat->N->N :=
	i n => (drop_N1 n i).

Recursive Definition
    drop_A : nat->A->A :=
	i a => (drop_A1 a i).

Lemma DROPM1 : (i:nat)(x:V)(ms:Ms)((drop_M i (sc x ms)) =
			    (sc (drop_V i x) (drop_Ms i ms))).

Lemma DROPM2 : (i:nat)(m:M)
	((drop_M i (lambda m)) = (lambda (drop_M (S i) m))).

Lemma DROPM3 : (i:nat)(drop_Ms i mnil)=mnil.

Lemma DROPM4 : (i:nat)(m:M)(ms:Ms)((drop_Ms i (mcons m ms)) = 
			    (mcons (drop_M i m) (drop_Ms i ms))).

Lemma DROPN1 : (i:nat)(n:N)((drop_N i (lam n)) = (lam (drop_N (S i) n))).

Lemma DROPN2 : (i:nat)(a:A)((drop_N i (an a)) = (an (drop_A i a))).

Lemma DROPN3 : (i:nat)(a:A)(n:N)
	((drop_A i (ap a n)) = (ap (drop_A i a) (drop_N i n))).

Lemma DROPN4 : (i:nat)(x:V)((drop_A i (var x)) = (var (drop_V i x))).