Declare ML Module "autocontra".

Grammar tactic simple_tactic :=
	[ "Auto_Contra" identarg($id)] ->
	[(TRY (auto_contra $id))].

Grammar tactic simple_tactic :=
	[ "Auto_Contra"] ->
	[(TRY (auto_contran))].

Require Bool.

Lemma bool_dec1
     : (b:bool)~(Is_true b)->(Is_true (negb b)).

Lemma bool_dec2
     : (b:bool)~b=true->(Is_true (negb b)).

Lemma bool_dec3
     : (b:bool)(Is_true b)->(b=true).

Lemma bool_dec4
     : (b:bool)~b=false->b=true.

Lemma bool_dec5
     : (b:bool)~b=true->b=false.

Lemma bool_dec6
     : (b:bool)b=false->~b=true.

Lemma bool_dec7
     : (b:bool)b=true->~b=false.

Section boolean_extension.

(* Giving if constructor over bool for general sets.*)

Hypothesis genset:Set.
Recursive Definition
    Setifb : bool->genset->genset->genset :=
	true x y => x |
	false x y => y.

Lemma orbor : (b1,b2:bool)
	(orb b1 b2)=true->b1=true\/b2=true.

End boolean_extension.

Lemma ororb : (b1,b2:bool)
	(b1=true\/b2=true)->(orb b1 b2)=true.

Lemma orbor1 :  (b1,b2:bool)
	(orb b1 b2)=false->b1=false/\b2=false.

Lemma ororb1 : (b1,b2:bool)
	(b1=false/\b2=false)->(orb b1 b2)=false.

Lemma sym_andb : (b1,b2:bool)
	(andb b1 b2)=(andb b2 b1).

Lemma andbf : (b:bool)
	(andb b false)=false.

Inductive
    lt : nat->nat->Prop :=
	lt_O : (i:nat)(lt O (S i)) |
	lt_S : (i,j:nat)(lt i j)->(lt (S i) (S j)).

Lemma S1 : (i,j:nat)(i=j)->~i=(S j).

Lemma S2 : (i,j:nat)(i=j)->~i=(S (S j)).

Lemma Splus : (i,j:nat)(plus i (S j))=(S (plus i j)).

Lemma Not_Splus : (i,j:nat)~(S (plus i j))=j.

Recursive Definition nateqb : nat->nat->bool :=
O O => true |
(S i) O => false |
O (S j) => false |
(S i) (S j) => (nateqb i j).

Lemma nateqb_sym : (i,j:nat)(nateqb i j)=(nateqb j i).

Lemma nateqb_is_eq1 : (i,j:nat)i=j->(nateqb i j)=true.

Lemma nateqb_is_eq2 : (i,j:nat)(nateqb i j)=true->i=j.

Lemma nateqb_is_eq3 : (i,j:nat)(~i=j)->(nateqb i j)=false.

Lemma nateqb_is_eq4 : (i,j:nat)((nateqb i j)=false)->~i=j.

Definition nat_compare1 : nat->nat->Prop :=
[i,j:nat]((nateqb i j)=true)\/(nateqb i j)=false.

Lemma nateqb_dec : (i,j:nat)(nat_compare1 i j).

Definition nat_compare : nat->nat->Prop :=
[i,j:nat]i=j\/~i=j.

Lemma nateq_dec : (i,j:nat)(nat_compare i j).

Lemma nateq_dec1 : (i,j:nat)(P:Prop)
		i=j->
		 ~i=j->
		  P.

Recursive Definition
    ltb : nat->nat->bool :=
	O O => false |
	O (S j) => true |
	(S i) O => false |
	(S i) (S j) => (ltb i j).

Lemma ltb_is_lt1 : (i,j:nat)
		(lt i j)->(ltb i j)=true.

Lemma ltb_is_lt2 : (i,j:nat)
		(ltb i j)=true->(lt i j).

Lemma ltb_is_lt3 : (i,j:nat)
		~(lt i j)->(ltb i j)=false.

Lemma ltb_is_lt4 : (i,j:nat)
		(ltb i j)=false->~(lt i j).

Lemma lt_not_eq1 : (i,j:nat)
		(lt i j)->~i=j.

Definition nat_compare2 : nat->nat->Prop :=
[i,j:nat](lt i j)\/i=j\/(lt j i).

Lemma natlt_dec : (i,j:nat)(nat_compare2 i j).

Lemma ltS : (i,j:nat)
		(lt i j)->(lt i (S j)).

Lemma ltSplus1 : (i,j:nat)
		(lt i (S (plus i j))).

Lemma ltSplus2 : (i,j:nat)
		(lt i (S (plus j i))).

Lemma ltSplus3 : (i,j,k:nat)
		(lt i j)->
		 (lt i (S (plus k j))).

Lemma ltplus1 : (i,j,k:nat)
		 (lt i k)->
		  (lt O j)->
		   (lt i (plus j k)).

Lemma plus_bridge : (i,j:nat)
		(plus i (S j))=(S (plus i j)).

Lemma Slt : (i,j:nat)
		(lt (S i) j)->
		 (lt i j).

Lemma notltbii : (i,j:nat)
		i=j->
		 (ltb i j)=false.

Lemma ltplus2 : (j,h,i:nat)
		(lt i h)->
		 (lt i (plus j h)).

Lemma lt_trans : (k,i,j:nat)
		(lt i j)->
		 (lt j k)->
		  (lt i k).

Lemma lt_trans1 : (i,k,j:nat)
		(lt i j)->
		 (lt j k)->
		  (lt (S i) k).

Lemma ltnotlt : (i,j:nat)
	(lt i j)->~(lt j i).

Lemma ltnot0 : (i,j:nat)
	(lt i j)->~j=O.

Lemma not_eq_notO_not_pred_eq : (i,j:nat)
	~i=O->
	 ~j=O->
	  ~i=j->
	   ~(pred i)=(pred j).

Lemma ltiSi : (i,j:nat)
	i=j->
	 (lt i (S j)).

Lemma notltii : (i,j:nat)
	i=j->
	 ~(lt i j).

Lemma ltS_ltpred : (i,j:nat)
	 (lt (S i) j)->
	  (lt i (pred j)).

Lemma ltpred_ltS : (i,j:nat)
	(lt i (pred j))->
	 (lt (S i) j).

Lemma lt_S_le : (j,i:nat)
	(lt i j)->
	 (S i)=j\/(lt (S i) j).

Lemma lt_S_le2 : (i,j:nat)
	(lt i (S j))->
	 (lt i j)\/i=j.

Lemma lt_trans2 : (i,j,k:nat) 
	(lt i (S j))->
	 (lt j k)->
	  (lt i k).

Lemma lt_trans3 : (i,j,k:nat)
	(lt i j)->
	 (lt j (S k))->
	  (lt i k).

Lemma not_lt_eq_lt : (i,j:nat)
	~(lt i j)->
	 i=j\/(lt j i).

Lemma ltS_neq_lt : (j,i:nat)
	(lt i (S j))->
	 ~i=j->
	  (lt i j).

Lemma lt_not_ltpred : (i,j:nat)
	(lt i j)->
	 ~(lt (pred j) i).

Lemma lt_not_ltS : (i,j:nat)
	(lt i j)->
	 ~(lt j (S i)).

Lemma plus_eq2 : (i,j:nat)
	(plus (S i) j)=
	 (S (plus i j)).

Lemma plus_right_id : (i:nat)
	(plus i O)=i.

Lemma sym_plus : (i,j:nat)
	(plus i j)=(plus j i).

Lemma ltS_not_lt : (i,j:nat)
	(lt i (S j))->
	 ~(lt j i).

Lemma ltplus3 : (i,j:nat)
	(lt O j)->
	 (lt i (plus j i)).

Lemma ltplus4 : (i,j,k:nat)
	(lt (plus i j) k)->
	 (lt i k).

Lemma ltplus6: (i,j,k,n:nat)
	(lt k i)->
	 (lt n j)->
	  (lt (plus k n) (plus i j)).

Lemma ltplus5: (k,j,i,n:nat)
	(lt (plus i j) (plus k n))->
	 (lt i k)\/(lt j k)\/(lt i n)\/(lt j n).

Recursive Definition
    max_nat : nat->nat->nat :=
	i j => (Setifb nat (ltb i j) j i).

Lemma max_nat0 : (i:nat)
	(max_nat i O)=i.

Lemma sym_max_nat : (i,j:nat)
	(max_nat i j)=(max_nat j i).

Lemma lt_max_nat : (i,j,k:nat)
	(lt i (S (max_nat j k)))->
	 ((lt i (S j)) /\ (lt k (S j)))\/
	  ((lt i (S k)) /\ (lt j (S k))).

Lemma eq_max_nat : (i,j,k:nat)
	i=(S (max_nat j k))->
	 (i=(S j)/\ (lt k (S j)))\/
	  (i=(S k)/\ (lt j (S k))).

Lemma lt_max_nat1 : (i,j,k:nat)
	i=j->
	 (lt i (S (max_nat j k))).

Lemma lt_max_nat2 :
	(i,j,k:nat)
	 (lt i j)->
	  (lt i (max_nat j k)).

Lemma S_max_nat_bridge0 :
	(i,j:nat)
	 (S (max_nat i j))=(max_nat (S i) (S j)).

(* Tactic syntax *)

Grammar tactic simple_tactic :=
	[ "NComp2" command:command($i) command:command($j)] ->
	[let $1 = <<(nat_compare2 $i $j)>> in
	 <:tactic:< Cut $1 ;
		[Destruct 1; [Intro | Destruct 1; Intro] | Auto]>>].

Grammar tactic simple_tactic :=
	[ "NComp" command:command($i) command:command($j)] ->
	[let $1 = <<(nat_compare $i $j)>> in
	 <:tactic:< Cut $1 ;
		 [Destruct 1; Intro |
		  Auto]>>].

Grammar tactic simple_tactic :=
	[ "Induction_clear" identarg($i)] ->
	[ <:tactic:<Induction $i; Clear $i>>].

Grammar tactic simple_tactic :=
	[ "Injection_clear" identarg($i)] ->
	[ <:tactic:<Injection $i; Clear $i; Intros>>].

Inductive F:Set :=
form: nat->F |
	(* Giving an infinite supply of decidably separate atomic Formulae.*)
Impl : F->F->F.
	(* So far, we are only dealing with implicational fragments.*)

Recursive Definition Feqb : F->F->bool :=
(form x) (form y) => (nateqb x y) |
(form x) (Impl P' Q') => false |
(Impl P Q) (form y) => false |
(Impl P Q) (Impl P' Q') => (andb (Feqb P P') (Feqb Q Q')).

Lemma Feqb_sym : (P,Q:F)(Feqb P Q)=(Feqb Q P).

Lemma Feqb_is_eq1 : (P,Q:F)(P=Q)->(Feqb P Q)=true.

Lemma Feqb_is_eq2 :
	(P,Q:F)(Feqb P Q)=true->P=Q.

Lemma Feqb_is_eq3 : (P,Q:F)(~P=Q)->(Feqb P Q)=false.

Lemma Feqb_is_eq4 : (P,Q:F)(Feqb P Q)=false->~P=Q.

Definition F_compare1 : F->F->Prop :=
[P,Q:F]((Feqb P Q)=true)\/(Feqb P Q)=false.

Lemma Feqb_dec : (P,Q:F)(F_compare1 P Q).

Definition F_compare : F->F->Prop :=
		[P,Q:F]P=Q\/~P=Q.

Lemma Feq_dec : (P,Q:F)(F_compare P Q).

Lemma Feq_dec1 : (i,j:F)(P:Prop)
		i=j->
		 ~i=j->
		  P.

Lemma Feq_dec2 : (i,j:F)(P:Prop)
		i=j->
		 ~i=j->
		  ~P.

(* Syntactic Definition Hyps := (list F). *)

Grammar command command3 :=
	["Hyps"] -> [$0=<<(list F)>>].

(* Syntactic Definition MT := (nil F). *)

Grammar command command3 :=
	["MT"] -> [$0=<<(nil F)>>].

(* Syntactic Definition Add_Hyp := (cons F). *)

Grammar command command3 :=
	["Add_Hyp" command:command($f) command:command($h)] ->
	[$0 = <<(cons F $f $h)>>].

Grammar command command3 :=
	["Len_Hyps" command:command($h)] ->
	[$0 = <<(length F $h)>>].

Lemma Add_Hyp1 :
	(i:Hyps)(P:F)~(Add_Hyp P i)=i.

Recursive Definition
    Hypseqb : Hyps->Hyps->bool :=
	MT MT => true |
	MT (Add_Hyp P' h') => false |
	(Add_Hyp P h) MT => false |
	(Add_Hyp P h) (Add_Hyp P' h') => (andb (Feqb P P') (Hypseqb h h')).

Lemma Hypseqb_sym :
	(i,j:Hyps)(Hypseqb i j)=(Hypseqb j i).

Lemma Hypseqb_is_eq1 :
	(i,j:Hyps)i=j->(Hypseqb i j)=true.

Lemma Hypseqb_is_eq2 :
	(i,j:Hyps)(Hypseqb i j)=true->i=j.

Lemma Hypseqb_is_eq3 :
	(i,j:Hyps)(~i=j)->(Hypseqb i j)=false.

Lemma Hypseqb_is_eq4 :
	(i,j:Hyps)(Hypseqb i j)=false->~i=j.

Definition Hyps_compare1 : Hyps->Hyps->Prop :=
[i,j:Hyps]((Hypseqb i j)=true)\/(Hypseqb i j)=false.

Lemma Hypseqb_dec :
	(i,j:Hyps)(Hyps_compare1 i j).

Definition Hyps_compare :Hyps->Hyps->Prop :=
	[i,j:Hyps]i=j\/~i=j.

Lemma Hypseq_dec :
	(i,j:Hyps)(Hyps_compare i j).

Inductive
    In_Hyps : nat->F->Hyps->Prop :=
	inhyps_base : (P:F)(h:Hyps)
			(In_Hyps O P (Add_Hyp P h)) |
	inhyps_rec : (n:nat)(P,Q:F)(h:Hyps)
			(In_Hyps n P h)->
			 (In_Hyps (S n) P (Add_Hyp Q h)).

Definition V :Set := nat.

Lemma In_lt :
	(h:Hyps)(x:V)(P:F)
	 (In_Hyps x P h)->
	  (lt x (Len_Hyps h)).

Inductive
    L:Set :=
	vr : V->L |
	app : V->L->L->L |
	lm : L->L.

Mutual Inductive
    M:Set :=
	sc : V->Ms->M |
	lambda : M->M
with
    Ms:Set :=
	mnil : Ms |
	mcons : M->Ms->Ms.

Scheme M_Ms_ind1 := Induction for M Sort Prop
  with Ms_M_ind1 := Induction for Ms Sort Prop.

(* We now join these two schemes together into the simultaneous 
induction scheme we actually want. *)

Lemma M_Ms_ind
     : (P:M->Prop)
        (P0:Ms->Prop)
         ((v:V)(m:Ms)(P0 m)->(P (sc v m)))
          ->((m:M)(P m)->(P (lambda m)))
             ->(P0 mnil)
                ->((m:M)(P m)->(m0:Ms)(P0 m0)->(P0 (mcons m m0)))
                  ->(((m:M)(P m)) /\ ((ms:Ms)(P0 ms))).

Mutual Inductive
    N:Set :=
	lam : N->N |
	an : A->N
with
    A:Set :=
	ap : A->N->A |
	var : V->A.

Scheme N_A_ind1 := Induction for N Sort Prop
  with A_N_ind1 := Induction for A Sort Prop.

Lemma N_A_ind     
     : (P:N->Prop)
        (P0:A->Prop)
         ((n:N)(P n)->(P (lam n)))
          ->((a:A)(P0 a)->(P (an a)))
             ->((a:A)(P0 a)->(n:N)(P n)->(P0 (ap a n)))
	          ->((v:V)(P0 (var v)))
		    ->(((n:N)(P n)) /\ ((a:A)(P0 a))).

Fixpoint
   theta [m:M]:N :=
	<N>Case m of
	    (* v;ms *)[x:V][ms:Ms]
		(theta1' ms (var x))
	    (* lambda m *)[m:M]
		(lam (theta m))
end with
    theta1' [ms:Ms]:A->N :=
	[a:A]<N>Case ms of
	    (* mnil *)
		(an a)
	    (* m::ms *)[m:M][ms:Ms]
		(theta1' ms (ap a (theta m)))
end.

(* Theta1' has its arguments in the wrong order so define theta'
in the same order as psi' later for ease of human parsing and consistency. *)

Recursive Definition theta' : A -> Ms -> N :=
a ms => (theta1' ms a).

Lemma th1 : (x:V)(ms:Ms)((theta (sc x ms)) = (theta' (var x) ms)).

Lemma th2 : (m:M)((theta (lambda m)) = (lam (theta m))).

Lemma th3 : (a:A)((theta' a mnil) = (an a)).

Lemma th4 : (m:M)(ms:Ms)(a:A)((theta' a (mcons m ms)) 
	= (theta' (ap a (theta m)) ms)).

Fixpoint
    psi [n:N]:M :=
	<M>Case n of
	    (* lam n *)[n:N]
		(lambda (psi n))
	    (* an a *)[a:A]
		(psi' a mnil)
end with
    psi' [a:A]:Ms->M :=
	[ms:Ms]<M>Case a of
	    (* ap a n *)[a':A][n:N]
		(psi' a' (mcons (psi n) ms))
	    (* var v *)[x:V]
		(sc x ms)
end.

Lemma ps1 : (n:N)((psi (lam n)) = (lambda (psi n))).

Lemma ps2 : (a:A)((psi (an a)) = (psi' a mnil)).

Lemma ps3 : (a:A)(n:N)(ms:Ms)((psi' (ap a n) ms) 
	= (psi' a (mcons (psi n) ms))).

Lemma ps4 : (x:V)(ms:Ms)((psi' (var x) ms) = (sc x ms)).

Definition thpsids :N->Prop :=
[n:N]((theta (psi n)) = n).

Definition thps'th's :A->Prop :=
[a:A](ms:Ms)((theta (psi' a ms)) = (theta' a ms)).

(*Now the actual proof *)

Lemma thpsid : ((n:N)(thpsids n))/\((a:A)(thps'th's a)).

Lemma thetapsi:
	(n:N)((theta(psi n)) = n).

Lemma thetapsi'theta':
	(a:A)(ms:Ms)((theta (psi' a ms)) = (theta' a ms)).

(* Because the bald statement of the proof has the wrong type
inferred, we define the lemmas individually and unfold them after
applying induction. *)

Definition psthids :M->Prop :=
[m:M]((psi (theta m)) = m).

Definition psth'ps's :Ms->Prop :=
[ms:Ms](a:A)((psi (theta' a ms)) = (psi' a ms)).

(* Now we actually state the lemma. *)

Lemma psthid : ((m:M)(psthids m))/\((ms:Ms)(psth'ps's ms)).

Lemma psitheta:
	(m:M)((psi(theta m))=m).

Lemma psitheta'psi':
	(ms:Ms)(a:A)((psi (theta' a ms)) = (psi' a ms)).

Recursive Definition lift_V : nat->V->V :=
i j => (Setifb V (ltb j i) j (S j)).

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

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

Recursive Definition
    lift_M : nat->M->M :=
	i m => (lift_M1 m i).

Recursive Definition
    lift_Ms : nat->Ms->Ms :=
	i ms => (lift_Ms1 ms i).

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

Recursive Definition lift_N : nat->N->N :=
i n => (lift_N1 n i).

Recursive Definition lift_A : nat->A->A :=
i a => (lift_A1 a i).

Lemma LIFTM1 : (i:nat)(x:V)(ms:Ms)
	((lift_M i (sc x ms)) =
	 (sc (lift_V i x) (lift_Ms i ms))).

Lemma LIFTM2 : (i:nat)(m:M)((lift_M i (lambda m)) = (lambda (lift_M (S i) m))).

Lemma LIFTM3 : (i:nat)(lift_Ms i mnil)=mnil.

Lemma LIFTM4 : (i:nat)(m:M)(ms:Ms)((lift_Ms i (mcons m ms)) = 
			    (mcons (lift_M i m) (lift_Ms i ms))).

Lemma LIFTN1 : (i:nat)(n:N)((lift_N i (lam n)) = (lam (lift_N (S i) n))).

Lemma LIFTN2 : (i:nat)(a:A)((lift_N i (an a)) = (an (lift_A i a))).

Lemma LIFTN3 : (i:nat)(a:A)(n:N)
	((lift_A i (ap a n)) = (ap (lift_A i a) (lift_N i n))).

Lemma LIFTN4 : (i:nat)(x:V)((lift_A i (var x)) = (var (lift_V i x))).

Lemma Lift_Lift_V_Bridge : (x:V)(i,j:nat)
	(lt i j)->
	 (lift_V i (lift_V j x))=
	  (lift_V (S j) (lift_V i x)).

Lemma Lift_Lift_L_Bridge : (l:L)(i,j:nat)
	(lt i j)->
	 (lift_L i (lift_L j l))=
	  (lift_L (S j) (lift_L i l)).

Definition lift_lift_n_bridge : N->Prop :=
	[n:N](i,j:nat)
	(lt i j)->
	 (lift_N i (lift_N j n))=
	  (lift_N (S j) (lift_N i n)).

Definition lift_lift_a_bridge : A->Prop :=
	[a:A](i,j:nat)
	(lt i j)->
	 (lift_A i (lift_A j a))=
	  (lift_A (S j) (lift_A i a)).

Lemma lift_lift_n_Bridge : 
	((n:N)(lift_lift_n_bridge n))/\
	 ((a:A)(lift_lift_a_bridge a)).

Lemma Lift_Lift_N_Bridge : 
	(n:N)(i,j:nat)
	(lt i j)->
	 (lift_N i (lift_N j n))=
	  (lift_N (S j) (lift_N i n)).

Lemma Lift_Lift_A_Bridge :
	(a:A)(i,j:nat)
	(lt i j)->
	 (lift_A i (lift_A j a))=
	  (lift_A (S j) (lift_A i a)).

Lemma Lift_Lift_V_Bridge0 : (x:V)(i,j:nat)
	(lt j i)->
	 (lift_V i (lift_V j x))=
	  (lift_V j (lift_V (pred i) x)).

Lemma Lift_Lift_L_Bridge0 : (l:L)(i,j:nat)
	(lt j i)->
	 (lift_L i (lift_L j l))=
	  (lift_L j (lift_L (pred i) l)).

Definition lift_lift_n_bridge0 : N->Prop :=
	[n:N](i,j:nat)
	(lt j i)->
	 (lift_N i (lift_N j n))=
	  (lift_N j (lift_N (pred i) n)).

Definition lift_lift_a_bridge0 : A->Prop :=
	[a:A](i,j:nat)
	(lt j i)->
	 (lift_A i (lift_A j a))=
	  (lift_A j (lift_A (pred i) a)).

Lemma lift_lift_n_Bridge0 : 
	((n:N)(lift_lift_n_bridge0 n))/\
	 ((a:A)(lift_lift_a_bridge0 a)).

Lemma Lift_Lift_N_Bridge0 : 
	(n:N)(i,j:nat)
	(lt j i)->
	 (lift_N i (lift_N j n))=
	  (lift_N j (lift_N (pred i) n)).

Lemma Lift_Lift_A_Bridge0 :
	(a:A)(i,j:nat)
	(lt j i)->
	 (lift_A i (lift_A j a))=
	  (lift_A j (lift_A (pred i) a)).

Lemma Lift_Lift_V_Bridge1 : (x:V)(i,j:nat)
	i=j->
	 (lift_V i (lift_V j x))=(lift_V (S j) (lift_V i x)).

Definition lift_lift_n_bridge1 : N->Prop :=
	[n:N](i,j:nat)
	 i=j->
	  (lift_N i (lift_N j n))=(lift_N (S j) (lift_N i n)).

Definition lift_lift_a_bridge1 : A->Prop :=
	[a:A](i,j:nat)
	 i=j->
	  (lift_A i (lift_A j a))=(lift_A (S j) (lift_A i a)).

Lemma lift_lift_n_Bridge1 : 
	((n:N)(lift_lift_n_bridge1 n))/\((a:A)(lift_lift_a_bridge1 a)).

Lemma Lift_Lift_N_Bridge1 :
	(n:N)(i,j:nat)
	 i=j->
	  (lift_N i (lift_N j n))=(lift_N (S j) (lift_N i n)).

Lemma  Lift_Lift_A_Bridge1 :
	(a:A)(i,j:nat)
	 i=j->
	  (lift_A i (lift_A j a))=(lift_A (S j) (lift_A i a)).

Lemma Lift_Lift_L_Bridge1 :(l:L)(i,j:nat)
	 i=j->
	  (lift_L i (lift_L j l))=(lift_L (S j) (lift_L i l)).

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

Inductive
    Occurs_In_V : nat->V->Prop :=
	Occurs_in_v : (i,j:nat)i=j->
		       (Occurs_In_V i j).

Inductive
    Occurs_In_L : nat->L->Prop :=
	Occurs_in_vr :
		(i:nat)(x:V)
		 (Occurs_In_V i x)->
		  (Occurs_In_L i (vr x)) |
	Occurs_in_app1 :
		(i:nat)(x:V)(l1,l2:L)
		 (Occurs_In_V i x)->
		  (Occurs_In_L i (app x l1 l2)) |
	Occurs_in_app2 :
		(i:nat)(x:V)(l1,l2:L)
		 (Occurs_In_L i l1)->
		  (Occurs_In_L i (app x l1 l2)) |
	Occurs_in_app3 :
		(i:nat)(x:V)(l1,l2:L)
		 (Occurs_In_L (S i) l2)->
		  (Occurs_In_L i (app x l1 l2)) |
	Occurs_in_lm :
		(i:nat)(l:L)
		 (Occurs_In_L (S i) l)->
		  (Occurs_In_L i (lm l)).

Mutual Inductive
    Occurs_In_M : nat->M->Prop :=
	Occurs_in_sc1 :
		(i:nat)(x:V)(ms:Ms)
		 (Occurs_In_V i x)->
		  (Occurs_In_M i (sc x ms)) |
	Occurs_in_sc2 :
		(i:nat)(x:V)(ms:Ms)
		 (Occurs_In_Ms i ms)->
		  (Occurs_In_M i (sc x ms)) |
	Occurs_in_lambda :
		(i:nat)(m:M)
		 (Occurs_In_M (S i) m)->
		  (Occurs_In_M i (lambda m))
with
    Occurs_In_Ms : nat->Ms->Prop :=
	Occurs_in_mcons1 :
		(i:nat)(m:M)(ms:Ms)
		 (Occurs_In_M i m)->
		  (Occurs_In_Ms i (mcons m ms)) |
	Occurs_in_mcons2 :
		(i:nat)(m:M)(ms:Ms)
		 (Occurs_In_Ms i ms)->
		  (Occurs_In_Ms i (mcons m ms)).

Mutual Inductive
    Occurs_In_N : nat->N->Prop :=
	Occurs_in_lam :
		(i:nat)(n:N)
		 (Occurs_In_N (S i) n)->
		  (Occurs_In_N i (lam n)) |
	Occurs_in_an :
		(i:nat)(a:A)
		 (Occurs_In_A i a)->
		  (Occurs_In_N i (an a))
with
    Occurs_In_A : nat->A->Prop :=
	Occurs_in_ap1 :
		(i:nat)(a:A)(n:N)
		 (Occurs_In_A i a)->
		  (Occurs_In_A i (ap a n)) |
	Occurs_in_ap2 :
		(i:nat)(a:A)(n:N)
		 (Occurs_In_N i n)->
		  (Occurs_In_A i (ap a n)) |
	Occurs_in_var :
		(i:nat)(x:V)
		 (Occurs_In_V i x)->
		  (Occurs_In_A i (var x)).

Recursive Definition Occurs_In_V1 : V->V->bool :=
i j => (nateqb i j).

Lemma OIV1_is_OIV1 : (i,x:V)
		(Occurs_In_V i x)->
		 (Occurs_In_V1 i x)=true.

Lemma OIV1_is_OIV2 : (i:V)(x:V)
		(Occurs_In_V1 i x)=true->
		 (Occurs_In_V i x).

Lemma OIV1_is_OIV3 : (i:V)(x:V)
		~(Occurs_In_V i x)->
		 (Occurs_In_V1 i x)=false.

Lemma OIV1_is_OIV4 : (i:V)(x:V)
		(Occurs_In_V1 i x)=false->
		 ~(Occurs_In_V i x).

Definition OIV_compare : V->V->Prop :=
[i:V][x:V](Occurs_In_V i x)\/~(Occurs_In_V i x).

Lemma OIV_dec :
	(i:V)(x:V)
	 (OIV_compare i x).

Recursive Definition
    Occurs_In_L1 : V->L->bool :=
	i (vr x) => (Occurs_In_V1 i x) |
	i (app  x l1 l2) =>
		(orb (Occurs_In_V1 i x)
		     (orb (Occurs_In_L1 i l1)
			  (Occurs_In_L1 (S i) l2))) |
	i (lm l) => (Occurs_In_L1 (S i) l).

Lemma OIL1_is_OIL1 :
	(l:L)(i:V)
	 (Occurs_In_L i l)->
	  (Occurs_In_L1 i l)=true.

Lemma OIL1_is_OIL2 : (l:L)(i:V)
		(Occurs_In_L1 i l)=true->
		 (Occurs_In_L i l).

Lemma OIL1_is_OIL3 :
	(l:L)(i:V)
	 ~(Occurs_In_L i l)->
	  (Occurs_In_L1 i l)=false.

Lemma OIL1_is_OIL4 :
	(l:L)(i:V)
	 (Occurs_In_L1 i l)=false->
	  ~(Occurs_In_L i l).

Definition OIL_compare : V->L->Prop :=
[i:V][l:L](Occurs_In_L i l)\/~(Occurs_In_L i l).

Lemma OIL_dec :
	(l:L)(i:V)
	 (OIL_compare i l).

Fixpoint
    Occurs_In_M2 [m:M] : V->bool :=
	[i:V]<bool>Case m of
	    (* x;ms *)[x:V][ms:Ms]
		(orb (Occurs_In_V1 i x) (Occurs_In_Ms2 ms i))
	    (* lambda m *)[m':M]
		(Occurs_In_M2 m' (S i))
end with
    Occurs_In_Ms2 [ms:Ms] : V->bool :=
	[i:V]<bool>Case ms of
	    (* mnil *)
		false
	    (* m::ms *)[m:M][ms':Ms]
		(orb (Occurs_In_M2 m i) (Occurs_In_Ms2 ms' i))
end.

Recursive Definition
    Occurs_In_M1 : V->M->bool :=
	x m => (Occurs_In_M2 m x).

Recursive Definition
    Occurs_In_Ms1 : V->Ms->bool :=
	x ms => (Occurs_In_Ms2 ms x).

Lemma OIM1 : (i,x:V)(ms:Ms)
	(Occurs_In_M1 i (sc x ms))
	=(orb (Occurs_In_V1 i x)
	      (Occurs_In_Ms1 i ms)).

Lemma OIM2 : (i:V)(m:M)
	(Occurs_In_M1 i (lambda m))=
	 (Occurs_In_M1 (S i) m).

Lemma OIM3 : (i:V)
	(Occurs_In_Ms1 i mnil)=false.

Lemma OIM4 : (i:V)(m:M)(ms:Ms)
	(Occurs_In_Ms1 i (mcons m ms))=
	 (orb (Occurs_In_M1 i m)
		(Occurs_In_Ms1 i ms)).

Definition oim1_is_oim1 : M->Prop :=
[m:M](i:V)(Occurs_In_M i m)->
	      (Occurs_In_M1 i m)=true.

Definition oims1_is_oims1 : Ms->Prop :=
[ms:Ms](i:V)(Occurs_In_Ms i ms)->
		(Occurs_In_Ms1 i ms)=true.

Lemma oiM1_is_oiM1 :
	((m:M)(oim1_is_oim1 m))/\
	 ((ms:Ms)(oims1_is_oims1 ms)).

Lemma OIM1_is_OIM1 : (i:V)(m:M)
(Occurs_In_M i m)->
	      (Occurs_In_M1 i m)=true.

Lemma OIMs1_is_OIMs1 : (i:V)(ms:Ms)
(Occurs_In_Ms i ms)->
		(Occurs_In_Ms1 i ms)=true.

Definition oim1_is_oim2 : M->Prop :=
[m:M](i:V)(Occurs_In_M1 i m)=true->
	      (Occurs_In_M i m).

Definition oims1_is_oims2 : Ms->Prop :=
[ms:Ms](i:V)(Occurs_In_Ms1 i ms)=true->
		(Occurs_In_Ms i ms).

Lemma oiM1_is_oiM2 :
	((m:M)(oim1_is_oim2 m))/\
	 ((ms:Ms)(oims1_is_oims2 ms)).

Lemma OIM1_is_OIM2 : (i:V)(m:M)
	(Occurs_In_M1 i m)=true->
	 (Occurs_In_M i m).

Lemma OIMs1_is_OIMs2 :
	(i:V)(ms:Ms)
	 (Occurs_In_Ms1 i ms)=true->
	  (Occurs_In_Ms i ms).

Lemma OIM1_is_OIM3 :
	(i:V)(m:M)
	 ~(Occurs_In_M i m)->
	  (Occurs_In_M1 i m)=false.

Lemma OIMs1_is_OIMs3 :
	(i:V)(ms:Ms)
	 ~(Occurs_In_Ms i ms)->
	  (Occurs_In_Ms1 i ms)=false.

Lemma OIM1_is_OIM4 :
	(i:V)(m:M)
	 (Occurs_In_M1 i m)=false->
	  ~(Occurs_In_M i m).

Lemma OIMs1_is_OIMs4 :
	(i:V)(ms:Ms)
	 (Occurs_In_Ms1 i ms)=false->
	  ~(Occurs_In_Ms i ms).

Definition OIM_compare : V->M->Prop :=
[i:V][m:M](Occurs_In_M i m)\/~(Occurs_In_M i m).

Lemma OIM_dec :
	(i:V)(m:M)
	 (OIM_compare i m).

Definition OIMs_compare : V->Ms->Prop :=
[i:V][ms:Ms](Occurs_In_Ms i ms)\/~(Occurs_In_Ms i ms).

Lemma OIMs_dec :
	(i:V)(ms:Ms)
	 (OIMs_compare i ms).

Fixpoint
    Occurs_In_N2 [n:N] : V->bool :=
	[i:V]<bool>Case n of
	    (* lam n *)[n':N]
		(Occurs_In_N2 n' (S i))
	    (* an a *)[a:A]
		(Occurs_In_A2 a i)
end with
    Occurs_In_A2 [a:A] : V->bool :=
	[i:V]<bool>Case a of
	    (* ap a n *)[a':A][n:N]
		(orb (Occurs_In_A2 a' i) (Occurs_In_N2 n i))
	    (* var x *)[x:V]
		(Occurs_In_V1 i x)
end.

Definition Occurs_In_N1 : V->N->bool :=
[i:V][n:N](Occurs_In_N2 n i).

Definition Occurs_In_A1 : V->A->bool :=
[i:V][a:A](Occurs_In_A2 a i).

Lemma OIN1 : (i:V)(n:N)
	(Occurs_In_N1 i (lam n))=
	 (Occurs_In_N1 (S i) n).

Lemma OIN2 : (i:V)(a:A)
	(Occurs_In_N1 i (an a))=
	 (Occurs_In_A1 i a).

Lemma OIN3 : (i:V)(a:A)(n:N)
	(Occurs_In_A1 i (ap a n))=
	 (orb (Occurs_In_A1 i a) (Occurs_In_N1 i n)).

Lemma OIN4 : (i,x:V)
	(Occurs_In_A1 i (var x))=
	 (Occurs_In_V1 i x).

Definition oin1_is_oin1 : N->Prop :=
	[n:N](i:V)
	 (Occurs_In_N i n)->
	  (Occurs_In_N1 i n)=true.

Definition oia1_is_oia1 : A->Prop :=
	[a:A](i:V)
	 (Occurs_In_A i a)->
	  (Occurs_In_A1 i a)=true.

Lemma oiN1_is_oiN1 :
	((n:N)(oin1_is_oin1 n))/\
	 ((a:A)(oia1_is_oia1 a)).

Lemma OIN1_is_OIN1 :
	(n:N)(i:V)
	 (Occurs_In_N i n)->
	  (Occurs_In_N1 i n)=true.

Lemma OIA1_is_OIA1 :
	(a:A)(i:V)
	 (Occurs_In_A i a)->
	  (Occurs_In_A1 i a)=true.

Definition oin1_is_oin2 : N->Prop :=
[n:N](i:V)(Occurs_In_N1 i n)=true->
	      (Occurs_In_N i n).

Definition oia1_is_oia2 : A->Prop :=
[a:A](i:V)(Occurs_In_A1 i a)=true->
	      (Occurs_In_A i a).

Lemma oiN1_is_oiN2 :
	((n:N)(oin1_is_oin2 n))/\
	 ((a:A)(oia1_is_oia2 a)).

Lemma OIN1_is_OIN2 :
	(n:N)(i:V)
	 (Occurs_In_N1 i n)=true->
	  (Occurs_In_N i n).

Lemma OIA1_is_OIA2 :
	(a:A)(i:V)
	 (Occurs_In_A1 i a)=true->
	  (Occurs_In_A i a).

Lemma OIN1_is_OIN3 :
	(i:V)(n:N)
	 ~(Occurs_In_N i n)->
	  (Occurs_In_N1 i n)=false.

Lemma OIA1_is_OIA3 :
	(i:V)(a:A)
	 ~(Occurs_In_A i a)->
	  (Occurs_In_A1 i a)=false.

Lemma OIN1_is_OIN4 :
	(i:V)(n:N)
	 (Occurs_In_N1 i n)=false->
	  ~(Occurs_In_N i n).

Lemma OIA1_is_OIA4 :
	(i:V)(a:A)
	 (Occurs_In_A1 i a)=false->
	  ~(Occurs_In_A i a).

Definition OIN_compare : V->N->Prop :=
[i:V][n:N](Occurs_In_N i n)\/~(Occurs_In_N i n).

Lemma OIN_dec :
	(i:V)(n:N)
	 (Occurs_In_N i n)\/~(Occurs_In_N i n).

Definition OIA_compare : V->A->Prop :=
[i:V][a:A](Occurs_In_A i a)\/~(Occurs_In_A i a).

Lemma OIA_dec :
	(i:V)(a:A)
	 (Occurs_In_A i a)\/~(Occurs_In_A i a).

Lemma NOI_Lift_V_Bridge0 :
	(x,i:V)
	 ~(Occurs_In_V i x)->
	  (lift_V i x)=
	   (lift_V (S i) x).

Definition NOI_lift_n_bridge0 : N->Prop :=
	[n:N](i:V)
	 ~(Occurs_In_N i n)->
	  (lift_N i n)=
	   (lift_N (S i) n).

Definition NOI_lift_a_bridge0 : A->Prop :=
	[a:A](i:V)
	 ~(Occurs_In_A i a)->
	  (lift_A i a)=
	   (lift_A (S i) a).

Lemma NOI_lift_n_Bridge0 :
	((n:N)(NOI_lift_n_bridge0 n))/\
	 ((a:A)(NOI_lift_a_bridge0 a)).

Lemma NOI_Lift_N_Bridge0 : 
	(n:N)(i:V)
	 ~(Occurs_In_N i n)->
	  (lift_N i n)=
	   (lift_N (S i) n).

Lemma NOI_Lift_A_Bridge0 :
	(a:A)(i:V)
	 ~(Occurs_In_A i a)->
	  (lift_A i a)=
	   (lift_A (S i) a).

Lemma NOI_Lift_L_Bridge0 :
	(l:L)(i:V)
	 ~(Occurs_In_L i l)->
	  (lift_L i l)=
	   (lift_L (S i) l).

Lemma NOI_Drop_V_Bridge0 :
	(x:V)(i,j:V)
	 (lt i j)->
	  ~(Occurs_In_V (S j) x)->
	   ~(Occurs_In_V j (drop_V i x)).

Definition noi_drop_m_bridge0 : M->Prop :=
	[m:M](i,j:V)
         (lt i j)
          ->~(Occurs_In_M (S j) m)
             ->~(Occurs_In_M j (drop_M i m)).

Definition noi_drop_ms_bridge0 : Ms->Prop :=
	[ms:Ms](i,j:V)
         (lt i j)
          ->~(Occurs_In_Ms (S j) ms)
             ->~(Occurs_In_Ms j (drop_Ms i ms)).

Lemma noi_drop_m_Bridge0 :
	((m:M)(noi_drop_m_bridge0 m))/\
	 ((ms:Ms)(noi_drop_ms_bridge0 ms)).

Lemma NOI_Drop_M_Bridge0 :
	(m:M)(i,j:V)
         (lt i j)
          ->~(Occurs_In_M (S j) m)
             ->~(Occurs_In_M j (drop_M i m)).

Lemma NOI_Drop_Ms_Bridge0 :
	(ms:Ms)(i,j:V)
         (lt i j)
          ->~(Occurs_In_Ms (S j) ms)
             ->~(Occurs_In_Ms j (drop_Ms i ms)).

Lemma NOI_Lift_V : (x:V)(i:nat)
	~(Occurs_In_V i (lift_V i x)).

Lemma NOI_Lift_V2 :(x:V)(i,j:nat)
	~(Occurs_In_V (S i) x)->
	 ~(Occurs_In_V i x)->
	  ~(Occurs_In_V (S i) (lift_V j x)).

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

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

Lemma NOI_lift_m : 
	((m:M)(noi_lift_m m))/\
	 ((ms:Ms)(noi_lift_ms ms)).

Lemma NOI_Lift_M :
	(m:M)(i:nat)
	 ~(Occurs_In_M i (lift_M i m)).

Lemma NOI_Lift_Ms :
	(ms:Ms)(i:nat)
	 ~(Occurs_In_Ms i (lift_Ms i ms)).

Definition noi_lift_m1 : M->Prop :=
	[m:M](i:nat)(j:nat)
	 ~(Occurs_In_M (S i) m)->
	  ~(Occurs_In_M i m)->
	   ~(Occurs_In_M (S i) (lift_M j m)).

Definition noi_lift_ms1 : Ms->Prop :=
	[ms:Ms](i:nat)(j:nat)
	 ~(Occurs_In_Ms (S i) ms)->
	  ~(Occurs_In_Ms i ms)->
	   ~(Occurs_In_Ms (S i) (lift_Ms j ms)).

Lemma NOI_lift_m1 : 
	((m:M)(noi_lift_m1 m))/\
	 ((ms:Ms)(noi_lift_ms1 ms)).

Lemma NOI_Lift_M1 :
	(m:M)(i,j:nat)
	 ~(Occurs_In_M (S i) m)->
	  ~(Occurs_In_M i m)->
	   ~(Occurs_In_M (S i) (lift_M j m)).

Lemma NOI_Lift_Ms1 :
	(ms:Ms)(i,j:nat)
	 ~(Occurs_In_Ms (S i) ms)->
	  ~(Occurs_In_Ms i ms)->
	   ~(Occurs_In_Ms (S i) (lift_Ms j ms)).

Lemma NOI_Lift_L : (l:L)(i:nat)
	~(Occurs_In_L i (lift_L i l)).

Lemma NOI_Lift_V3 : (x:V)(i,j:nat)
	(lt j i)->
	 ~(Occurs_In_V i x)->
	  ~(Occurs_In_V (S i) (lift_V j x)).

Lemma NOI_Lift_V4 : (x:V)(i,j:nat)
	j=i->
	 ~(Occurs_In_V i x)->
	  ~(Occurs_In_V (S i) (lift_V j x)).

(* 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.

(* Support functions for Phi. *)

(* subst a for i in (var j). *)
Recursive Definition
    VsubstAV : A->V->V->A :=
	a i j => (Setifb A (nateqb i j) a (var (drop_V i j))).

Fixpoint
    NsubstAV1 [n:N]: A->nat->N :=
	[a:A][i:nat]<N>Case n of
	    (* lam n *)[n':N]
		(lam (NsubstAV1 n' (lift_A O a) (S i)))
	    (* an a *)[a':A]
		(an (AsubstAV1 a' a i))
end with
    AsubstAV1 [a:A] : A->nat->A :=
	[a':A][i:nat]<A>Case a of
	    (* ap a n *)[a'':A][n:N]
		(ap (AsubstAV1 a'' a' i) (NsubstAV1 n a' i))
	    (* var x *)[x:V]
		(VsubstAV a' i x)
end.

Recursive Definition
    NsubstAV : A->V->N->N :=
	a i n => (NsubstAV1 n a i).

Recursive Definition
    AsubstAV : A->V->A->A :=
	a i a' => (AsubstAV1 a' a i).

Lemma NSAV1 : (a:A)(i:nat)(n:N)
		((NsubstAV a i (lam n)) =
		 (lam (NsubstAV (lift_A O a) (S i) n))).

Lemma NSAV2 : (a:A)(i:nat)(a':A)
		((NsubstAV a i (an a')) =
		 (an (AsubstAV a i a'))).

Lemma NSAV3 : (a:A)(i:nat)(a':A)(n:N)
		((AsubstAV a i (ap a' n)) =
		 (ap (AsubstAV a i a') (NsubstAV a i n))).

Lemma NSAV4 : (a:A)(i:nat)(x:V)
		((AsubstAV a i (var x)) =
		 (VsubstAV a i x)).

(* The Mapping Phi from LJ to NJ. *)
Recursive Definition
    phi : L -> N :=
	(vr x) => (an (var x)) |
	(app x l1 l2) =>
		(NsubstAV (ap (var x) (phi l1)) O (phi l2)) |
	(lm l) => (lam (phi l)).

(* The Mapping PhiBar from LJ to MJ. *)
Recursive Definition
    phibar : L->M :=
	(vr x) => (sc x mnil) |
	(app x l1 l2) =>
		(MsubstVMV x (phibar l1) O (phibar l2)) |
	(lm l) => (lambda (phibar l)).

Definition lift_psi_bridge : N->Prop :=
[n:N](i:nat)(lift_M i (psi n)) = (psi (lift_N i n)).

Definition lift_psi'_bridge : A->Prop :=
[a:A](ms:Ms)(i:nat)(lift_M i (psi' a ms))=(psi' (lift_A i a) (lift_Ms i ms)).

Lemma Lift_psi_Bridge : 
           ((n:N)(lift_psi_bridge n))/\
           ((a:A)(lift_psi'_bridge a)).

Lemma Lift_Psi_Bridge : (n:N)(i:nat)(lift_M i (psi n)) = (psi (lift_N i n)).

Lemma Lift_Psi'_Bridge : (a:A)(ms:Ms)(i:nat)
(lift_M i (psi' a ms))=(psi' (lift_A i a) (lift_Ms i ms)).

Lemma Lift_Theta_Bridge : 
	(m:M)(i:nat)(lift_N i (theta m)) = (theta (lift_M i m)).

Lemma Lift_Theta'_Bridge : (a:A)(ms:Ms)(i:nat)
(lift_N i (theta' a ms))=(theta' (lift_A i a) (lift_Ms i ms)).

Lemma Lift_Lift_M_Bridge : 
	(m:M)(i,j:nat)
	 (lt i j)->
	  (lift_M i (lift_M j m))=
	   (lift_M (S j) (lift_M i m)).

Lemma Lift_Lift_Ms_Bridge : 
	(ms:Ms)(i,j:nat)
	 (lt i j)->
	  (lift_Ms i (lift_Ms j ms))=
	   (lift_Ms (S j) (lift_Ms i ms)).

Lemma Lift_Lift_M_Bridge0 : 
	(m:M)(i,j:nat)
	 (lt j i)->
	  (lift_M i (lift_M j m))=
	   (lift_M j (lift_M (pred i) m)).

Lemma Lift_Lift_Ms_Bridge0 : 
	(ms:Ms)(i,j:nat)
	 (lt j i)->
	  (lift_Ms i (lift_Ms j ms))=
	   (lift_Ms j (lift_Ms (pred i) ms)).

Lemma Lift_Lift_M_Bridge1 : 
	(m:M)(i,j:nat)
	 i=j->
	  (lift_M i (lift_M j m))=
	   (lift_M (S j) (lift_M i m)).

Lemma Lift_Lift_Ms_Bridge1 : 
	(ms:Ms)(i,j:nat)
	 i=j->
	  (lift_Ms i (lift_Ms j ms))=
	   (lift_Ms (S j) (lift_Ms i ms)).

Definition msub_psi_bridge : N->Prop :=
	[n2:N](n1:N)(x,y:V)
	 (MsubstVMV x (psi n1) y (psi n2))=
	  (psi (NsubstAV (ap (var x) n1) y n2)).

Definition msub_psi'_bridge : A->Prop :=
	[a:A](x:V)(n:N)(y:V)(ms:Ms)
	 (MsubstVMV x (psi n) y (psi' a ms))=
	  (psi' (AsubstAV (ap (var x) n) y a) (MssubstVMV x (psi n) y ms)).

Lemma Msub_psi_bridge : 
	((n:N)(msub_psi_bridge n))/\((a:A)(msub_psi'_bridge a)).

Lemma Msub_Psi_Bridge :
	(n2:N)(n1:N)(x,y:V)
	 (MsubstVMV x (psi n1) y (psi n2))=
	  (psi (NsubstAV (ap (var x) n1) y n2)).

Lemma Msub_Psi'_Bridge :
	(a:A)(x:V)(n:N)(y:V)(ms:Ms)
	 (MsubstVMV x (psi n) y (psi' a ms))=
	  (psi' (AsubstAV (ap (var x) n) y a) (MssubstVMV x (psi n) y ms)).

Lemma Nsub_Theta_Bridge :
	(x:V)(m1:M)(y:V)(m2:M)
	 (NsubstAV (ap (var x) (theta m1)) y (theta m2))
	  =(theta (MsubstVMV x m1 y m2)).

Definition theta_drop_m_bridge : M->Prop :=
	[m:M](i:nat)(theta (drop_M i m))=(drop_N i (theta m)).

Definition theta'_drop_ms_bridge : Ms->Prop :=
	[ms:Ms](a:A)(i:nat)
	(theta' (drop_A i a) (drop_Ms i ms))=(drop_N i (theta' a ms)).

Lemma theta_drop_M_bridge :
	((m:M)(theta_drop_m_bridge m))/\
	 ((ms:Ms)(theta'_drop_ms_bridge ms)).

Lemma Theta_Drop_M_Bridge :
	(m:M)(i:nat)(theta (drop_M i m))=(drop_N i (theta m)).

Lemma Theta'_Drop_Ms_Bridge :
	(ms:Ms)(a:A)(i:nat)
	 (theta' (drop_A i a) (drop_Ms i ms))=(drop_N i (theta' a ms)).

Lemma Psi_Drop_N_Bridge :
	(n:N)(i:nat)
	 (psi (drop_N i n))=(drop_M i (psi n)).

Lemma Psi'_Drop_A_Bridge :
	(a:A)(ms:Ms)(i:nat)
	 (psi' (drop_A i a) (drop_Ms i ms))=(drop_M i (psi' a ms)).

Lemma thetaphibarphi : (l:L)(theta (phibar l))=(phi l).

Lemma psiphiphibar : (l:L)(psi (phi l))=(phibar l).

Lemma OI_Lift_V1_1: 
	(x:V)(i,j:nat)
	 (lt i j)->
	  (Occurs_In_V1 i (lift_V j x))=(Occurs_In_V1 i x).

Lemma OI_Lift_V1_2:
	(x:V)(i,j:nat)
	 i=j->
	  (Occurs_In_V1 i (lift_V j x))=false.

Lemma OI_Lift_V1_3 :
	(x:V)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_V1 (S i) (lift_V j x))=
	   (Occurs_In_V1 i x).

Lemma OI_Lift_V1_4 : (x:V)(i,j:nat)
	(lt j i)->
	 (Occurs_In_V1 i (lift_V j x))=
	  (Occurs_In_V1 (pred i) x).

Definition oi_lift_m1_1: M->Prop :=
	[m:M](i,j:nat)
	 (lt i j)->(Occurs_In_M1 i (lift_M j m))=(Occurs_In_M1 i m).

Definition oi_lift_ms1_1: Ms->Prop :=
	[ms:Ms](i,j:nat)
	 (lt i j)->
	  (Occurs_In_Ms1 i (lift_Ms j ms))=(Occurs_In_Ms1 i ms).

Lemma oi_lift_M1_1 :
	((m:M)(oi_lift_m1_1 m))/\
	 ((ms:Ms)(oi_lift_ms1_1 ms)).

Lemma OI_Lift_M1_1:
	(m:M)(i,j:nat)
	 (lt i j)->
	  (Occurs_In_M1 i (lift_M j m))=(Occurs_In_M1 i m).

Lemma OI_Lift_Ms1_1:
	(ms:Ms)(i,j:nat)
	 (lt i j)->
	  (Occurs_In_Ms1 i (lift_Ms j ms))=(Occurs_In_Ms1 i ms).

Definition oi_lift_m1_2: M->Prop :=
	[m:M](i,j:nat)
	 i=j->(Occurs_In_M1 i (lift_M j m))=false.

Definition oi_lift_ms1_2: Ms->Prop :=
	[ms:Ms](i,j:nat)
	 i=j->(Occurs_In_Ms1 i (lift_Ms j ms))=false.

Lemma oi_lift_M1_2 :
	((m:M)(oi_lift_m1_2 m))/\
	 ((ms:Ms)(oi_lift_ms1_2 ms)).

Lemma OI_Lift_M1_2:
	(m:M)(i,j:nat)
	 i=j->
	  (Occurs_In_M1 i (lift_M j m))=false.

Lemma OI_Lift_Ms1_2:
	(ms:Ms)(i,j:nat)
	 i=j->
	  (Occurs_In_Ms1 i (lift_Ms j ms))=false.

Definition oi_lift_m1_3: M->Prop :=
	[m:M](i,j:nat)
	 (lt j i)->
	  (Occurs_In_M1 (S i) (lift_M j m))=(Occurs_In_M1 i m).

Definition oi_lift_ms1_3: Ms->Prop :=
	[ms:Ms](i,j:nat)
	 (lt j i)->
	  (Occurs_In_Ms1 (S i) (lift_Ms j ms))=(Occurs_In_Ms1 i ms).

Lemma oi_lift_M1_3 :
	((m:M)(oi_lift_m1_3 m))/\
	 ((ms:Ms)(oi_lift_ms1_3 ms)).

Lemma OI_Lift_M1_3:
	(m:M)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_M1 (S i) (lift_M j m))=(Occurs_In_M1 i m).

Lemma OI_Lift_Ms1_3:
	(ms:Ms)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_Ms1 (S i) (lift_Ms j ms))=(Occurs_In_Ms1 i ms).

Definition oi_lift_m1_4: M->Prop :=
	[m:M](i,j:nat)
	 (lt j i)->
	  (Occurs_In_M1 i (lift_M j m))=(Occurs_In_M1 (pred i) m).

Definition oi_lift_ms1_4: Ms->Prop :=
	[ms:Ms](i,j:nat)
	 (lt j i)->
	  (Occurs_In_Ms1 i (lift_Ms j ms))=
	   (Occurs_In_Ms1 (pred i) ms).

Lemma oi_lift_M1_4 :
	((m:M)(oi_lift_m1_4 m))/\
	 ((ms:Ms)(oi_lift_ms1_4 ms)).

Lemma OI_Lift_M1_4 :
	(m:M)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_M1 i (lift_M j m))=(Occurs_In_M1 (pred i) m).

Lemma OI_Lift_Ms1_4 :
	(ms:Ms)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_Ms1 i (lift_Ms j ms))=
	   (Occurs_In_Ms1 (pred i) ms).

Definition oi_lift_n1_1: N->Prop :=
	[n:N](i,j:nat)
	 (lt i j)->(Occurs_In_N1 i (lift_N j n))=(Occurs_In_N1 i n).

Definition oi_lift_a1_1: A->Prop :=
	[a:A](i,j:nat)
	 (lt i j)->(Occurs_In_A1 i (lift_A j a))=(Occurs_In_A1 i a).

Lemma oi_lift_N1_1 :
	((n:N)(oi_lift_n1_1 n))/\
	 ((a:A)(oi_lift_a1_1 a)).

Lemma OI_Lift_N1_1:
	(n:N)(i,j:nat)
	 (lt i j)->
	  (Occurs_In_N1 i (lift_N j n))=(Occurs_In_N1 i n).

Lemma OI_Lift_A1_1:
	(a:A)(i,j:nat)
	 (lt i j)->
	  (Occurs_In_A1 i (lift_A j a))=(Occurs_In_A1 i a).

Definition oi_lift_n1_2 : N->Prop :=
	[n:N](i,j:nat)
	 i=j->(Occurs_In_N1 i (lift_N j n))=false.

Definition oi_lift_a1_2 : A->Prop :=
	[a:A](i,j:nat)
	 i=j->(Occurs_In_A1 i (lift_A j a))=false.

Lemma oi_lift_N1_2 :
	((n:N)(oi_lift_n1_2 n))/\
	 ((a:A)(oi_lift_a1_2 a)).

Lemma OI_Lift_N1_2:
	(n:N)(i,j:nat)
	 i=j->
	  (Occurs_In_N1 i (lift_N j n))=false.

Lemma OI_Lift_A1_2:
	(a:A)(i,j:nat)
	 i=j->
	  (Occurs_In_A1 i (lift_A j a))=false.

Definition oi_lift_n1_3: N->Prop :=
	[n:N](i,j:nat)
	 (lt j i)->
	  (Occurs_In_N1 (S i) (lift_N j n))=(Occurs_In_N1 i n).

Definition oi_lift_a1_3: A->Prop :=
	[a:A](i,j:nat)
	 (lt j i)->
	  (Occurs_In_A1 (S i) (lift_A j a))=(Occurs_In_A1 i a).

Lemma oi_lift_N1_3 : 
	((n:N)(oi_lift_n1_3 n))/\
	 ((a:A)(oi_lift_a1_3 a)).

Lemma OI_Lift_N1_3 :
	(n:N)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_N1 (S i) (lift_N j n))=(Occurs_In_N1 i n).

Lemma OI_Lift_A1_3 :	
	(a:A)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_A1 (S i) (lift_A j a))=(Occurs_In_A1 i a).

Definition oi_lift_n1_4: N->Prop :=
	[n:N](i,j:nat)
	 (lt j i)->
	  (Occurs_In_N1 i (lift_N j n))=(Occurs_In_N1 (pred i) n).

Definition oi_lift_a1_4: A->Prop :=
	[a:A](i,j:nat)
	 (lt j i)->
	  (Occurs_In_A1 i (lift_A j a))=(Occurs_In_A1 (pred i) a).

Lemma oi_lift_N1_4 : 
	((n:N)(oi_lift_n1_4 n))/\
	 ((a:A)(oi_lift_a1_4 a)).

Lemma OI_Lift_N1_4 :
	(n:N)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_N1 i (lift_N j n))=(Occurs_In_N1 (pred i) n).

Lemma OI_Lift_A1_4 :
	(a:A)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_A1 i (lift_A j a))=(Occurs_In_A1 (pred i) a).

Lemma OI_Lift_L1_4 :
	(l:L)(i,j:nat)
	 (lt j i)->
	  (Occurs_In_L1 i (lift_L j l))=
	   (Occurs_In_L1 (pred i) l).

Definition noi_msub_b_bridge : M->Prop :=
	[m:M](x:V)(m1:M)(i:nat)
	 ~(Occurs_In_M i m)->
	  (MsubstVMV x m1 i m)=(drop_M i m).

Definition noi_mssub_b_bridge : Ms->Prop :=
	[ms:Ms](x:V)(m1:M)(i:nat)
	 ~(Occurs_In_Ms i ms)->
	  (MssubstVMV x m1 i ms)=(drop_Ms i ms).

Lemma noi_msub_b_Bridge :
	((m:M)(noi_msub_b_bridge m))/\
	 ((ms:Ms)(noi_mssub_b_bridge ms)).

Lemma NOI_Msub_Bridge :
	(m:M)(x:V)(m1:M)(i:nat)
	 ~(Occurs_In_M i m)->
	  (MsubstVMV x m1 i m)=(drop_M i m).

Lemma NOI_Mssub_Bridge :
	(ms:Ms)(x:V)(m1:M)(i:nat)
	 ~(Occurs_In_Ms i ms)->
	  (MssubstVMV x m1 i ms)=(drop_Ms i ms).

Lemma Lift_Drop_V_Bridge1 : (x:V)(i,j:nat)
	(lt j i)->
	 ~(Occurs_In_V j x)->
	  (lift_V i (drop_V j x))=
	   (drop_V j (lift_V (S i) x)).

Definition lift_drop_n_bridge1 : N->Prop :=
	[n:N](i,j:nat)
	 (lt j i)->
	  ~(Occurs_In_N j n)->
	   (lift_N i (drop_N j n))=
	    (drop_N j (lift_N (S i) n)).

Definition lift_drop_a_bridge1 : A->Prop :=
	[a:A](i,j:nat)
	 (lt j i)->
	  ~(Occurs_In_A j a)->
	   (lift_A i (drop_A j a))=
	    (drop_A j (lift_A (S i) a)).

Lemma lift_drop_n_Bridge1 :
	((n:N)(lift_drop_n_bridge1 n))/\((a:A)(lift_drop_a_bridge1 a)).

Lemma Lift_Drop_N_Bridge1 :
	(n:N)(i,j:nat)
	 (lt j i)->
	  ~(Occurs_In_N j n)->
	   (lift_N i (drop_N j n))=
	    (drop_N j (lift_N (S i) n)).

Lemma Lift_Drop_A_Bridge1 :
	(a:A)(i,j:nat)
	 (lt j i)->
	  ~(Occurs_In_A j a)->
	   (lift_A i (drop_A j a))=
	    (drop_A j (lift_A (S i) a)).

Lemma Drop_Lift_V_Bridge1 :
	(x:V)(i,j:nat)
	 ~(Occurs_In_V i x)->
	  (lt j (S i))->
	   (drop_V (S i) (lift_V j x))=
	    (lift_V j (drop_V i x)).

Definition drop_lift_n_bridge1 : N->Prop :=
	[n:N](i,j:nat)
	 ~(Occurs_In_N i n)->
	  (lt j (S i))->
	   (drop_N (S i) (lift_N j n))=
	    (lift_N j (drop_N i n)).

Definition drop_lift_a_bridge1 : A->Prop :=
	[a:A](i,j:nat)
	 ~(Occurs_In_A i a)->
	  (lt j (S i))->
	   (drop_A (S i) (lift_A j a))=
	    (lift_A j (drop_A i a)).

Lemma drop_lift_n_Bridge1 :
	((n:N)(drop_lift_n_bridge1 n))/\
	 ((a:A)(drop_lift_a_bridge1 a)).

Lemma Drop_Lift_N_Bridge1 :
	(n:N)(i,j:nat)
	 ~(Occurs_In_N i n)->
	  (lt j (S i))->
	   (drop_N (S i) (lift_N j n))=
	    (lift_N j (drop_N i n)).

Lemma Drop_Lift_A_Bridge1 :
	(a:A)(i,j:nat)
	 ~(Occurs_In_A i a)->
	  (lt j (S i))->
	   (drop_A (S i) (lift_A j a))=
	    (lift_A j (drop_A i a)).

Lemma Lift_Vsub_Bridge0 : 
	(x:V)(i,j:nat)(a:A)
	 (lt i j)->
	  (lift_A j (VsubstAV a i x))=
	   (VsubstAV (lift_A j a) i (lift_V (S j) x)).

Definition lift_nsub_b_bridge0 : N->Prop :=
	[n:N](i,j:nat)(a:A)
	 (lt i j)->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) i (lift_N (S j) n)).

Definition lift_asub_b_bridge0 : A->Prop :=
	[a:A](i,j:nat)(a1:A)
	 (lt i j)->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) i (lift_A (S j) a)).

Lemma lift_nsub_b_Bridge0 :
	((n:N)(lift_nsub_b_bridge0 n))/\ ((a:A)(lift_asub_b_bridge0 a)).

Lemma Lift_Nsub_Bridge0 :
	(n:N)(i,j:nat)(a:A)
	 (lt i j)->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) i (lift_N (S j) n)).

Lemma Lift_Asub_Bridge0 :
	(a:A)(i,j:nat)(a1:A)
	 (lt i j)->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) i (lift_A (S j) a)).

Lemma Lift_Msub_Bridge0 :
	(x:V)(m,m0:M)(i,j:nat)
	 (lt i j)->
	  (lift_M j (MsubstVMV x m i m0))=
	   (MsubstVMV (lift_V j x) (lift_M j m) i (lift_M (S j) m0)).

Lemma Lift_Mssub_Bridge0 :
	(x:V)(m:M)(ms:Ms)(i,j:nat)
	 (lt i j)->
	  (lift_Ms j (MssubstVMV x m i ms))=
	   (MssubstVMV (lift_V j x) (lift_M j m) i (lift_Ms (S j) ms)).

Definition lift_msub_bridge2 : M->Prop :=
	[m:M](x,y:V)(m1:M)
	 (MsubstVMV x m1 (S y) (lift_M y (lift_M (S y) m)))=
	  (MsubstVMV x m1 y (lift_M (S (S y)) (lift_M (S y) m))).

Definition lift_mssub_bridge2 : Ms->Prop :=
	[ms:Ms](x,y:V)(m1:M)
	 (MssubstVMV x m1 (S y) (lift_Ms y (lift_Ms (S y) ms)))=
	  (MssubstVMV x m1 y (lift_Ms (S (S y)) (lift_Ms (S y) ms))).

Lemma Lift_msub_bridge2 :
	((m:M)(lift_msub_bridge2 m))/\
	 ((ms:Ms)(lift_mssub_bridge2 ms)).

Lemma Lift_Msub_Bridge2 :
	(x:V)(m1:M)(y:V)(m:M)
	 (MsubstVMV x m1 (S y) (lift_M y (lift_M (S y) m)))=
	  (MsubstVMV x m1 y (lift_M (S (S y)) (lift_M (S y) m))).

Lemma Lift_Mssub_Bridge2 :
	(x:V)(m1:M)(y:V)(ms:Ms)
	 (MssubstVMV x m1 (S y) (lift_Ms y (lift_Ms (S y) ms)))=
	  (MssubstVMV x m1 y (lift_Ms (S (S y)) (lift_Ms (S y) ms))).

Lemma Lift_Vsub_Bridge1 : 
	(x:V)(i,j:nat)(a:A)
	 i=j->
	  (lift_A j (VsubstAV a i x))=
	   (VsubstAV (lift_A j a) i (lift_V (S j) x)).

Lemma Lift_Vsub_Bridge2 : 
	(x:V)(i,j:nat)(a:A)
	 (lt j i)->
	  (lift_A j (VsubstAV a i x))=
	   (VsubstAV (lift_A j a) (S i) (lift_V j x)).

Definition lift_nsub_b_bridge1 : N->Prop :=
	[n:N](i,j:nat)(a:A)
	 i=j->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) i (lift_N (S j) n)).

Definition lift_asub_b_bridge1 : A->Prop :=
	[a:A](i,j:nat)(a1:A)
	 i=j->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) i (lift_A (S j) a)).

Lemma lift_nsub_b_Bridge1 :
	((n:N)(lift_nsub_b_bridge1 n))/\ ((a:A)(lift_asub_b_bridge1 a)).

Lemma Lift_Nsub_Bridge1 :
	(n:N)(i,j:nat)(a:A)
	 i=j->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) i (lift_N (S j) n)).

Lemma Lift_Asub_Bridge1 :
	(a:A)(i,j:nat)(a1:A)
	 i=j->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) i (lift_A (S j) a)).

Definition lift_nsub_b_bridge2 : N->Prop :=
	[n:N](i,j:nat)(a:A)
	 (lt j i)->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) (S i) (lift_N j n)).

Definition lift_asub_b_bridge2 : A->Prop :=
	[a:A](i,j:nat)(a1:A)
	 (lt j i)->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) (S i) (lift_A j a)).

Lemma lift_nsub_b_Bridge2 :
	((n:N)(lift_nsub_b_bridge2 n))/\ ((a:A)(lift_asub_b_bridge2 a)).

Lemma Lift_Nsub_Bridge2 :
	(n:N)(i,j:nat)(a:A)
	 (lt j i)->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) (S i) (lift_N j n)).

Lemma Lift_Asub_Bridge2 :
	(a:A)(i,j:nat)(a1:A)
	 (lt j i)->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) (S i) (lift_A j a)).

Lemma Lift_Vsub_Bridge3 : 
	(x:V)(i,j:nat)(a:A)
	 i=j->
	  (lift_A j (VsubstAV a i x))=
	   (VsubstAV (lift_A j a) (S i) (lift_V j x)).

Definition lift_nsub_b_bridge3 : N->Prop :=
	[n:N](i,j:nat)(a:A)
	 i=j->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) (S i) (lift_N j n)).

Definition lift_asub_b_bridge3 : A->Prop :=
	[a:A](i,j:nat)(a1:A)
	 i=j->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) (S i) (lift_A j a)).

Lemma lift_nsub_b_Bridge3 :
	((n:N)(lift_nsub_b_bridge3 n))/\ ((a:A)(lift_asub_b_bridge3 a)).

Lemma Lift_Nsub_Bridge3 :
	(n:N)(i,j:nat)(a:A)
	 i=j->
	  (lift_N j (NsubstAV a i n))=
	   (NsubstAV (lift_A j a) (S i) (lift_N j n)).

Lemma Lift_Asub_Bridge3 :
	(a:A)(i,j:nat)(a1:A)
	 i=j->
	  (lift_A j (AsubstAV a1 i a))=
	   (AsubstAV (lift_A j a1) (S i) (lift_A j a)).

Lemma Lift_Msub_Bridge1 :
	(x:V)(m,m0:M)(i,j:nat)
	 i=j->
	  (lift_M j (MsubstVMV x m i m0))=
	   (MsubstVMV (lift_V j x) (lift_M j m) i (lift_M (S j) m0)).

Lemma Lift_Mssub_Bridge1 :
	(x:V)(m:M)(ms:Ms)(i,j:nat)
	 i=j->
	  (lift_Ms j (MssubstVMV x m i ms))=
	   (MssubstVMV (lift_V j x) (lift_M j m) i (lift_Ms (S j) ms)).

Lemma Lift_Phi_Bridge : 
	(l:L)(i:nat)
	 (lift_N i (phi l))=
	  (phi (lift_L i l)).

Lemma Lift_PhiBar_Bridge :
	(l:L)(i:nat)
	 (lift_M i (phibar l))=
	  (phibar (lift_L i l)).

Lemma Drop_Lift_L :
	(l:L)(x:V)
	 (drop_L x (lift_L x l))=l.

Definition oi_theta : M->Prop :=
	[m:M](x:V)
	 (Occurs_In_M x m)->
	  (Occurs_In_N x (theta m)).

Definition oi_theta' : Ms->Prop :=
	[ms:Ms](a:A)(x:V)
	 ((Occurs_In_Ms x ms)\/(Occurs_In_A x a))->
	  (Occurs_In_N x (theta' a ms)).

Lemma OI_theta :
	((m:M)(oi_theta m))/\
	 ((ms:Ms)(oi_theta' ms)).

Lemma OI_Theta :
	(m:M)(x:V)
	 (Occurs_In_M x m)->
	  (Occurs_In_N x (theta m)).

Lemma OI_Theta' :
	(ms:Ms)(a:A)(x:V)
	 ((Occurs_In_Ms x ms)\/(Occurs_In_A x a))->
	  (Occurs_In_N x (theta' a ms)).

Definition oi_psi : N->Prop :=
	[n:N](x:V)
	 (Occurs_In_N x n)->
	  (Occurs_In_M x (psi n)).

Definition oi_psi' : A->Prop :=
	[a:A](ms:Ms)(x:V)
	 ((Occurs_In_A x a)\/(Occurs_In_Ms x ms))->
	  (Occurs_In_M x (psi' a ms)).

Lemma OI_psi :
	((n:N)(oi_psi n))/\
	 ((a:A)(oi_psi' a)).

Lemma OI_Psi :
	(n:N)(x:V)
	 (Occurs_In_N x n)->
	  (Occurs_In_M x (psi n)).

Lemma OI_Psi' :
	(a:A)(ms:Ms)(x:V)
	 ((Occurs_In_A x a)\/(Occurs_In_Ms x ms))->
	  (Occurs_In_M x (psi' a ms)).

Definition noi_theta : M->Prop :=
	[m:M](x:V)
	 ~(Occurs_In_M x m)->
	  ~(Occurs_In_N x (theta m)).

Definition noi_theta' : Ms->Prop :=
	[ms:Ms](x:V)(a:A)
	 ~(Occurs_In_Ms x ms)->
	  ~(Occurs_In_A x a)->
	   ~(Occurs_In_N x (theta' a ms)).

Lemma noi_Theta :
	((m:M)(noi_theta m))/\
	 ((ms:Ms)(noi_theta' ms)).

Lemma NOI_Theta :
	(x:V)(m:M)
	~(Occurs_In_M x m)->
	  ~(Occurs_In_N x (theta m)).

Lemma NOI_Theta' :
	(x:V)(a:A)(ms:Ms)
	 ~(Occurs_In_A x a)->
	  ~(Occurs_In_Ms x ms)->
	   ~(Occurs_In_N x (theta' a ms)).

Recursive Definition
    Height_L : L->nat :=
	(vr x) => O |
	(app x l1 l2) => (S (max_nat (Height_L l1) (Height_L l2))) |
	(lm l) => (S (Height_L l)).

Definition
    lt_Height_L : L->L->Prop :=
	[l1,l2:L](lt (Height_L l1) (Height_L l2)).

Lemma WF_Height_L :
	(well_founded L lt_Height_L).

Lemma L_Height_ind1 :
	(P:L->Prop)
	 ((l0:L)((l1:L)(lt_Height_L l1 l0)->(P l1))->(P l0))->
	  (l:L)(P l).

Lemma L_Height_ind :
	(P:L->Prop)
	 ((l0:L)((l1:L)(lt (Height_L l1) (Height_L l0))->(P l1))->(P l0))->
	  (l:L)(P l).

Lemma Height_Lift_L :
	(l:L)(i:nat)
	 (Height_L (lift_L i l))=
	  (Height_L l).

Fixpoint
    Height_M [m:M] : nat :=
	<nat>Case m of
	(* sc x ms *)[x:V][ms:Ms](S (Height_Ms ms))
	(* lambda m *)[m:M](S (Height_M m))
	end with
    Height_Ms [ms:Ms] : nat :=
	<nat>Case ms of
	(* mnil *)O
	(* mcons m ms *)[m:M][ms:Ms](S (max_nat (Height_M m) (Height_Ms ms)))
	end.

Lemma HTM1 : (x:V)(ms:Ms)
	(Height_M (sc x ms))=(S (Height_Ms ms)).

Lemma HTM2 : (m:M)
	(Height_M (lambda m))=(S (Height_M m)).

Lemma HTM3 :
	(Height_Ms mnil)=O.

Lemma HTM4 : (m:M)(ms:Ms)
	(Height_Ms (mcons m ms))=(S (max_nat (Height_M m) (Height_Ms ms))).

Lemma Height_Ms_Zero_Nil1 : (ms:Ms)
	~ms=mnil->
	 (lt O (Height_Ms ms)).

Lemma Height_Ms_Zero_Nil : (ms:Ms)
	(Height_Ms ms)=O->
	 ms=mnil.

Lemma Height_M_not_eq_not_eq :
	(m:M)(m0:M)
	 ~(Height_M m)=(Height_M m0)->
	  ~m=m0.

Lemma Height_Ms_not_eq_not_eq :
	(ms:Ms)(ms0:Ms)
	 ~(Height_Ms ms)=(Height_Ms ms0)->
	  ~ms=ms0.

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

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

Lemma height_lift_M :
	((m:M)(height_lift_m m))/\
	 ((ms:Ms)(height_lift_ms ms)).

Lemma Height_Lift_M :
	(m:M)(i:nat)
	 (Height_M (lift_M i m))=
	  (Height_M m).

Lemma Height_Lift_Ms :
	(ms:Ms)(i:nat)
	 (Height_Ms (lift_Ms i ms))=
	  (Height_Ms ms).

Section HeightMind.

Variable P:M->Prop.
Variable P0:Ms->Prop.

Definition QSM : M->Prop :=
	[m:M]
	 ((m1:M)
	   ((lt (Height_M m1) (Height_M m)) \/
	     (Height_M m1)=(Height_M m))->
	    (P m1))/\
	 ((ms1:Ms)
	   ((lt (Height_Ms ms1) (Height_M m)) \/
	     (Height_Ms ms1)=(Height_M m))->
	    (P0 ms1)).

Definition QSMs : Ms->Prop :=
	[ms:Ms]
	 ((m1:M)
	   ((lt (Height_M m1) (Height_Ms ms)) \/
	     (Height_M m1)=(Height_Ms ms))->
	    (P m1))/\
	 ((ms1:Ms)
	   ((lt (Height_Ms ms1) (Height_Ms ms)) \/
	     (Height_Ms ms1)=(Height_Ms ms))->
	    (P0 ms1)).

Lemma M_Ms_szind1 :
	(((m:M)(QSM m))/\((ms:Ms)(QSMs ms)))->
	 ((m:M)(P m))/\((ms:Ms)(P0 ms)).

Lemma M_Ms_Height_ind :
   ((m:M)
     (((m1:M)(lt (Height_M m1) (Height_M m))->(P m1)) /\
     ((ms1:Ms)(lt (Height_Ms ms1) (Height_M m))->(P0 ms1)))->(P m))->
     ((ms:Ms)
        (((ms1:Ms)(lt (Height_Ms ms1) (Height_Ms ms))->(P0 ms1))/\
        ((m1:M)(lt (Height_M m1) (Height_Ms ms))->(P m1)))->(P0 ms))->
         ((m:M)(P m))/\((ms:Ms)(P0 ms)).

Recursive Definition
    lifts_V : nat->nat->V->V :=
	O j x => x |
	(S i) j x => (lift_V j (lifts_V i j x)).

Recursive Definition
    lifts_L : nat->nat->L->L :=
	i j (vr x) => (vr (lifts_V i j x)) |
	i j (app x l l0) =>
		(app (lifts_V i j x) (lifts_L i j l) (lifts_L i (S j) l0)) |
	i j (lm l) => (lm (lifts_L i (S j) l)).

Fixpoint
    lifts_M1 [m:M] : nat->nat->M :=
	[i,j:nat]
	<M>Case m of
	    (* x;ms *)[x:V][ms:Ms]
		(sc (lifts_V i j x) (lifts_Ms1 ms i j))
	    (* \m *)[m:M]
		(lambda (lifts_M1 m i (S j)))
	end
with
    lifts_Ms1 [ms:Ms] : nat->nat->Ms :=
	[i,j:nat]
	<Ms>Case ms of
	    (* mnil *)mnil
	    (* m::ms *)[m:M][ms:Ms]
		(mcons (lifts_M1 m i j) (lifts_Ms1 ms i j))
	end.

Recursive Definition lifts_M : nat->nat->M->M :=
i j m => (lifts_M1 m i j).

Recursive Definition lifts_Ms : nat->nat->Ms->Ms :=
i j ms => (lifts_Ms1 ms i j).

Lemma LIFTSM1 : (i,j:nat)(x:V)(ms:Ms)
	(lifts_M i j (sc x ms))=
	 (sc (lifts_V i j x) (lifts_Ms i j ms)).

Lemma LIFTSM2 : (i,j:nat)(m:M)
	(lifts_M i j (lambda m))=
	 (lambda (lifts_M i (S j) m)).

Lemma LIFTSM3 : (i,j:nat)
	(lifts_Ms i j mnil)=mnil.

Lemma LIFTSM4 : (i,j:nat)(m:M)(ms:Ms)
	(lifts_Ms i j (mcons m ms))=
	 (mcons (lifts_M i j m) (lifts_Ms i j ms)).

Lemma Lifts_L0 : (l:L)(j:nat)
	(lifts_L O j l)=l.

Definition lifts_m0 : M->Prop :=
	[m:M](j:nat)
	 (lifts_M O j m)=m.

Definition lifts_ms0 : Ms->Prop :=
	[ms:Ms](j:nat)
	 (lifts_Ms O j ms)=ms.

Lemma Lifts_m0 :
	((m:M)(lifts_m0 m))/\
	 ((ms:Ms)(lifts_ms0 ms)).

Lemma Lifts_M0 :
	(m:M)(j:nat)
	 (lifts_M O j m)=m.

Lemma Lifts_Ms0 :
	(ms:Ms)(j:nat)
	 (lifts_Ms O j ms)=ms.

Lemma Lifts_L_rec1 : (l:L)(i,j:nat)
	(lifts_L (S i) j l)=(lift_L j (lifts_L i j l)).

Definition lifts_m_rec1 : M->Prop :=
	[m:M](i,j:nat)
	 (lifts_M (S i) j m)=(lift_M j (lifts_M i j m)).

Definition lifts_ms_rec1 : Ms->Prop :=
	[ms:Ms](i,j:nat)
	 (lifts_Ms (S i) j ms)=(lift_Ms j (lifts_Ms i j ms)).

Lemma Lifts_m_rec1 :
	((m:M)(lifts_m_rec1 m))/\
	 ((ms:Ms)(lifts_ms_rec1 ms)).

Lemma Lifts_M_rec1 :
	(m:M)(i,j:nat)
	 (lifts_M (S i) j m)=(lift_M j (lifts_M i j m)).

Lemma Lifts_Ms_rec1 :
	(ms:Ms)(i,j:nat)
	 (lifts_Ms (S i) j ms)=(lift_Ms j (lifts_Ms i j ms)).

Lemma Lifts_V_rec2 :
	(x:V)(i,j:nat)
	 (lifts_V (S i) j x)=
	  (lifts_V i j (lift_V j x)).

Lemma Lifts_L_rec2 :
	(l:L)(i,j:nat)
	 (lifts_L (S i) j l)=
	  (lifts_L i j (lift_L j l)).

Definition lifts_m_rec2 : M->Prop :=
	[m:M](i,j:nat)
	 (lifts_M (S i) j m)=(lifts_M i j (lift_M j m)).

Definition lifts_ms_rec2 : Ms->Prop :=
	[ms:Ms](i,j:nat)
	 (lifts_Ms (S i) j ms)=(lifts_Ms i j (lift_Ms j ms)).

Lemma Lifts_m_rec2 :
	((m:M)(lifts_m_rec2 m))/\
	 ((ms:Ms)(lifts_ms_rec2 ms)).

Lemma Lifts_M_rec2 :
	(m:M)(i,j:nat)
	 (lifts_M (S i) j m)=(lifts_M i j (lift_M j m)).

Lemma Lifts_Ms_rec2 :
	(ms:Ms)(i,j:nat)
	 (lifts_Ms (S i) j ms)=(lifts_Ms i j (lift_Ms j ms)).

Lemma Lifts_Msub_Bridge0 :
	(k:nat)(x:V)(m,m0:M)(i,j:nat)
	 (lt i j)->
	  (lifts_M k j (MsubstVMV x m0 i m))=
	   (MsubstVMV (lifts_V k j x) (lifts_M k j m0) i (lifts_M k (S j) m)).

Lemma Lifts_Mssub_Bridge0 :
	(k:nat)(x:V)(ms:Ms)(m0:M)(i,j:nat)
	 (lt i j)->
	  (lifts_Ms k j (MssubstVMV x m0 i ms))=
	   (MssubstVMV (lifts_V k j x)
		       (lifts_M k j m0)
		       i
		       (lifts_Ms k (S j) ms)).

Lemma Lifts_Msub_Bridge1 :
	(k:nat)(x:V)(m,m0:M)(i,j:nat)
	 i=j->
	  (lifts_M k j (MsubstVMV x m0 i m))=
	   (MsubstVMV (lifts_V k j x) (lifts_M k j m0) i (lifts_M k (S j) m)).

Lemma Lifts_Mssub_Bridge1 :
	(k:nat)(x:V)(ms:Ms)(m0:M)(i,j:nat)
	 i=j->
	  (lifts_Ms k j (MssubstVMV x m0 i ms))=
	   (MssubstVMV (lifts_V k j x)
		       (lifts_M k j m0)
		       i
		       (lifts_Ms k (S j) ms)).

Lemma Lifts_PhiBar_Bridge : (l:L)(i,j:nat)
	(lifts_M i j (phibar l))=
	 (phibar (lifts_L i j l)).

Lemma Lifts_Lift_V_Bridge3 :
	(x:V)(i,j,k:nat)
	 ~(lt k j)->
	   (lifts_V i j (lift_V k x))=
	    (lift_V (plus i k) (lifts_V i j x)).

Lemma Lifts_Lift_L_Bridge3 :
	(l:L)(i,j,k:nat)
	 ~(lt k j)->
	   (lifts_L i j (lift_L k l))=
	    (lift_L (plus i k) (lifts_L i j l)).

Lemma Lifts_Lifts_L_Bridge0 :
	(i,j,k,n:nat)(l:L)
	 k=n->
	  (lifts_L i k (lifts_L j n l))=
	   (lifts_L (plus i j) n l).

(* The Mapping RhoBar from MJ to LJ. *)
Fixpoint
    rhobar [m:M] : L :=
	<L>Case m of
	    (* x;ms *)[x:V][ms:Ms]
		<L>Case ms of
		    (* mnil *)
			(vr x)
		    (* m::ms *)[m:M][ms:Ms]
			(app x (rhobar m) (rhobar' ms (S O)))
		end
	    (* \m *)[m:M]
		(lm (rhobar m))
	end
with
    rhobar' [ms:Ms] : nat->L :=
	[i:nat]
	<L>Case ms of
	    (* mnil *)
		(vr O)
	    (* m::ms *)[m:M][ms:Ms]
		(app O (lifts_L i O (rhobar m)) (rhobar' ms (S i)))
	end.

Recursive Definition rhobar1 : nat->Ms->L :=
i ms => (rhobar' ms i).

Recursive Definition rho : N->L :=
n => (rhobar (psi n)).

Lemma rhothetarhobar : (m:M)
	(rho (theta m))=(rhobar m).

Lemma Rhobar1 : (x:V)
	(rhobar (sc x mnil))=(vr x).

Lemma Rhobar2 : (x:V)(m:M)
	(rhobar (sc x (mcons m mnil)))=
	 (app x (rhobar m) (vr O)).

Lemma Rhobar3 : (x:V)(m:M)(ms:Ms)
	(rhobar (sc x (mcons m ms)))=
	 (app x (rhobar m) (rhobar1 (S O) ms)).

Lemma Rhobar4 : (m:M)
	(rhobar (lambda m))=(lm (rhobar m)).

Lemma Rhobar5 : (i:nat)
	(rhobar1 i mnil)=(vr O).

Lemma Rhobar6 : (m:M)(ms:Ms)(i:nat)
	(rhobar1 i (mcons m ms))=
	 (app O
	      (lifts_L i O (rhobar m))
	      (rhobar1 (S i) ms)).

Definition phibarrhobar1 : M->Prop :=
	[m:M]
	 (phibar (rhobar m))=m.

Definition phibarrhobar2 : Ms->Prop :=
	[ms:Ms]
	 (m:M)(i:nat)
	  ((m1:M)
	    (lt (Height_M m1) (Height_Ms (mcons m ms)))->
	     (phibar (rhobar m1))=m1)->
	   (phibar (rhobar1 i (mcons m ms)))=
	    (sc O (lifts_Ms i O (mcons m ms))).

Lemma Phibarrhobar :
	((m:M)(phibarrhobar1 m))/\
	 ((ms:Ms)(phibarrhobar2 ms)).

Lemma phibarrhobar :
	(m:M)(phibar (rhobar m))=m.

Lemma phibarrhobar_ms :
	(i:nat)(m:M)(ms:Ms)
	 (phibar (rhobar1 i (mcons m ms)))=
	    (sc O (lifts_Ms i O (mcons m ms))).

Lemma phirho : (n:N)(phi (rho n))=n.

Inductive
    L_Deriv : Hyps -> L -> F -> Prop :=
	L_Axiom :
		(h:Hyps)(i:V)(P:F)
		 (In_Hyps i P h)->
		  (L_Deriv h (vr i) P) |
	Implies_L :
		(h:Hyps)(i:V)(P:F)(Q:F)(l1:L)(l2:L)(R:F)
		 (In_Hyps i (Impl P Q) h)->
		  (L_Deriv h l1 P)->
		   (L_Deriv (Add_Hyp Q h) l2 R)->
		    (L_Deriv h (app i l1 l2) R) |
	Implies_R :
		(h:Hyps)(P:F)(l:L)(Q:F)
		 (L_Deriv (Add_Hyp P h) l Q)->
		  (L_Deriv h (lm l) (Impl P Q)).

Scheme L_Deriv_ind1 := Induction for L_Deriv Sort Prop.
(* New Induction scheme for inductive Proposition.*)

Mutual Inductive
    M_Deriv : Hyps -> M -> F -> Prop :=
	Choose :
		(h:Hyps)(i:V)(P:F)(ms:Ms)(R:F)
		 (In_Hyps i P h)->
		  (Ms_Deriv h P ms R)->
		   (M_Deriv h (sc i ms) R) |
	Abstract :
		(h:Hyps)(P:F)(m:M)(Q:F)
		 (M_Deriv (Add_Hyp P h) m Q)->
		  (M_Deriv h (lambda m) (Impl P Q))
with
    Ms_Deriv : Hyps -> F -> Ms -> F -> Prop :=
	Meet :
		(h:Hyps)(P:F)
		 (Ms_Deriv h P mnil P) |
	Implies_S :
		(h:Hyps)(m:M)(P:F)(Q:F)(ms:Ms)(R:F)
		 (M_Deriv h m P)->
		  (Ms_Deriv h Q ms R)->
		   (Ms_Deriv h (Impl P Q) (mcons m ms) R).

Scheme M_Ms_Deriv_ind1 := Induction for M_Deriv Sort Prop
  with Ms_M_Deriv_ind1 := Induction for Ms_Deriv Sort Prop.

Lemma M_Ms_Deriv_ind :
	(P:(h:Hyps)(m:M)(f:F)(M_Deriv h m f)->Prop)
	(P0:(h:Hyps)(f:F)(m:Ms)(f0:F)(Ms_Deriv h f m f0)->Prop)
	 ((h:Hyps)(i:V)(P1:F)(ms:Ms)(R:F)
	  (i0:(In_Hyps i P1 h))
	   (m:(Ms_Deriv h P1 ms R))
	    (P0 h P1 ms R m)->
	     (P h (sc i ms) R (Choose h i P1 ms R i0 m)))->
	 ((h:Hyps)(P1:F)(m:M)(Q:F)
	  (m0:(M_Deriv (Add_Hyp P1 h) m Q))
	   (P (Add_Hyp P1 h) m Q m0)->
	    (P h (lambda m) (Impl P1 Q) (Abstract h P1 m Q m0)))->
	 ((h:Hyps)(P1:F)(P0 h P1 mnil P1 (Meet h P1)))->
	 ((h:Hyps)(m:M)(P1,Q:F)(ms:Ms)(R:F)
	  (m0:(M_Deriv h m P1))
	   (P h m P1 m0)->
	    (m1:(Ms_Deriv h Q ms R))
	     (P0 h Q ms R m1)->
	      (P0 h (Impl P1 Q) (mcons m ms) R
	        (Implies_S h m P1 Q ms R m0 m1)))->
	  ((h:Hyps)(m:M)(f:F)(m0:(M_Deriv h m f))(P h m f m0))/\
	  ((h:Hyps)(f:F)(m:Ms)(f0:F)(m0:(Ms_Deriv h f m f0))(P0 h f m f0 m0)).

Mutual Inductive
    N_Deduc : Hyps -> N -> F -> Prop :=
	Implies_I :
		(h:Hyps)(P:F)(n:N)(Q:F)
		 (N_Deduc (Add_Hyp P h) n Q)->
		  (N_Deduc h (lam n) (Impl P Q)) |
	AN_Axiom :
		(h:Hyps)(a:A)(P:F)
		 (A_Deduc h a P)->
		  (N_Deduc h (an a) P)
with
    A_Deduc : Hyps -> A -> F -> Prop :=
	Implies_E :
		(h:Hyps)(a:A)(P:F)(Q:F)(n:N)
		 (A_Deduc h a (Impl P Q))->
		  (N_Deduc h n P)->
		   (A_Deduc h (ap a n) Q) |
	A_Axiom :
		(h:Hyps)(i:V)(P:F)
		 (In_Hyps i P h)->
		  (A_Deduc h (var i) P).

Scheme N_A_Deduc_ind1 := Induction for N_Deduc Sort Prop
  with A_N_Deduc_ind1 := Induction for A_Deduc Sort Prop.

Lemma N_A_Deduc_ind
     : (P:(h:Hyps)(n:N)(f:F)(N_Deduc h n f)->Prop)
        (P0:(h:Hyps)(a:A)(f:F)(A_Deduc h a f)->Prop)
          ((h:Hyps)
           (P1:F)
            (n:N)
             (Q:F)
              (n0:(N_Deduc (Add_Hyp P1 h) n Q))
               (P (Add_Hyp P1 h) n Q n0)
                ->(P h (lam n) (Impl P1 Q) (Implies_I h P1 n Q n0)))
          ->((h:Hyps)
              (a:A)
               (P1:F)
                (a0:(A_Deduc h a P1))
                 (P0 h a P1 a0)->(P h (an a) P1 (AN_Axiom h a P1 a0)))
             ->((h:Hyps)
                 (a:A)
                  (P1,Q:F)
                   (n:N)
                    (a0:(A_Deduc h a (Impl P1 Q)))
                     (P0 h a (Impl P1 Q) a0)
                      ->(n0:(N_Deduc h n P1))
                         (P h n P1 n0)
                          ->(P0 h (ap a n) Q
                              (Implies_E h a P1 Q n a0 n0)))
                ->((h:Hyps)
                    (i:V)
                     (P1:F)
                      (i0:(In_Hyps i P1 h))
                       (P0 h (var i) P1 (A_Axiom h i P1 i0)))
                   ->((h:Hyps)(n:N)(f:F)(n0:(N_Deduc h n f))(P h n f n0))/\
		     ((h:Hyps)(a:A)(f:F)(a0:(A_Deduc h a f))(P0 h a f a0)).

Definition m_admis_psi :
	(h:Hyps)(n:N)(R:F)(N_Deduc h n R)-> Prop :=
	 [h:Hyps][n:N][R:F][prf:(N_Deduc h n R)](M_Deriv h (psi n) R).

Definition m_admis_psi' :
	(h:Hyps)(a:A)(P:F)(A_Deduc h a P)->Prop :=
	 [h:Hyps][a:A][P:F][prf:(A_Deduc h a P)]
	  (R:F)(ms:Ms)((Ms_Deriv h P ms R) -> (M_Deriv h (psi' a ms) R)).

Lemma M_admis_psi :
	((h:Hyps)(n:N)(R:F)(prf:(N_Deduc h n R))(m_admis_psi h n R prf))/\
	 ((h:Hyps)(a:A)(R:F)(prf:(A_Deduc h a R))(m_admis_psi' h a R prf)).

Lemma M_Admis_Psi :
	(h:Hyps)(n:N)(R:F)
	 (N_Deduc h n R)->
	  (M_Deriv h (psi n) R).

Lemma M_Admis_Psi' :
	(h:Hyps)(a:A)(ms:Ms)(R:F)(P:F)
	 (A_Deduc h a P)->
	  (Ms_Deriv h P ms R)->
	   (M_Deriv h (psi' a ms) R).

Definition n_admis_theta : (h:Hyps)(m:M)(P:F)(M_Deriv h m P)->Prop :=
[h:Hyps][m:M][R:F][prf:(M_Deriv h m R)](N_Deduc h (theta m) R).

Definition n_admis_theta' :
	(h:Hyps)(P:F)(ms:Ms)(R:F)(Ms_Deriv h P ms R)->Prop :=
	 [h:Hyps][P:F][ms:Ms][R:F][prf:(Ms_Deriv h P ms R)]
	  (a:A)((A_Deduc h a P) -> (N_Deduc h (theta' a ms) R)).

Lemma N_admis_theta :
	((h:Hyps)(m:M)(P:F)(prf:(M_Deriv h m P))(n_admis_theta h m P prf)) /\
	 ((h:Hyps)(P:F)(ms:Ms)(R:F)(prf:(Ms_Deriv h P ms R))
		(n_admis_theta' h P ms R prf)).

Lemma N_Admis_Theta :
	(h:Hyps)(m:M)(R:F)
	 (M_Deriv h m R)->
	  (N_Deduc h (theta m) R).

Lemma N_Admis_Theta' :
	(h:Hyps)(P:F)(ms:Ms)(R:F)
	 (Ms_Deriv h P ms R)->
	 ((a:A)((A_Deduc h a P)-> 
	  (N_Deduc h (theta' a ms) R))).

Recursive Definition
    Weaken_Hyps : nat->F->Hyps->Hyps :=
	O P h => (Add_Hyp P h) |
	(S n) P MT => MT |
	(S n) P (Add_Hyp Q h) => (Add_Hyp Q (Weaken_Hyps n P h)).

Lemma In_Weaken_Hyps :
	(i,j:nat)(h:Hyps)(P,Q:F)
	 (lt j (S (Len_Hyps h)))->
	  (In_Hyps i P h)->
	   (In_Hyps (lift_V j i) P (Weaken_Hyps j Q h)).

Definition n_admis_weaken :
	(h:Hyps)(n:N)(P:F)(N_Deduc h n P)->Prop :=
	 [h:Hyps][n:N][P:F][D:(N_Deduc h n P)]
	  (j:nat)(Q:F)
	   (lt j (S (Len_Hyps h)))->
	    (N_Deduc (Weaken_Hyps j Q h) (lift_N j n) P).

Definition a_admis_weaken :
	(h:Hyps)(a:A)(P:F)(A_Deduc h a P)->Prop :=
	 [h:Hyps][a:A][P:F][D:(A_Deduc h a P)]
	  (j:nat)(Q:F)
	   (lt j (S (Len_Hyps h)))->
	    (A_Deduc (Weaken_Hyps j Q h) (lift_A j a) P).

Lemma N_admis_weaken :
	((h:Hyps)(n:N)(R:F)(n0:(N_Deduc h n R))(n_admis_weaken h n R n0))/\
	 ((h:Hyps)(a:A)(R:F)(a0:(A_Deduc h a R))(a_admis_weaken h a R a0)).

Lemma N_Admis_Weaken :
	(h:Hyps)(n:N)(P:F)(j:nat)(Q:F)
	 (N_Deduc h n P)->
	   (lt j (S (Len_Hyps h)))->
	    (N_Deduc (Weaken_Hyps j Q h) (lift_N j n) P).

Lemma A_Admis_Weaken :
	(h:Hyps)(a:A)(P:F)(j:nat)(Q:F)
	 (A_Deduc h a P)->
	   (lt j (S (Len_Hyps h)))->
	    (A_Deduc (Weaken_Hyps j Q h) (lift_A j a) P).

Definition l_admis_weaken :
	(h:Hyps)(l:L)(P:F)(L_Deriv h l P)->Prop :=
	 [h:Hyps][l:L][P:F][D:(L_Deriv h l P)]
	  (j:nat)(Q:F)
	   (lt j (S (Len_Hyps h)))->
	    (L_Deriv (Weaken_Hyps j Q h) (lift_L j l) P).

Lemma L_admis_weaken :
	(h:Hyps)(l:L)(P:F)(D:(L_Deriv h l P))
	 (l_admis_weaken h l P D).

Lemma L_Admis_Weaken :
	(h:Hyps)(l:L)(P,Q:F)(j:nat)
	 (L_Deriv h l P)->
	  (lt j (S (Len_Hyps h)))->
	   (L_Deriv (Weaken_Hyps j Q h) (lift_L j l) P).

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

Lemma Drop_S_Bridge_nat :
	(i,j:nat)
	 ~i=j->
	  (drop_V (S i) (S j))=
	   (S (drop_V i j)).

Lemma In_Strength :
	(h:Hyps)(i,j:nat)(P:F)
	 (In_Hyps i P h)->
	  ~i=j->
	   (In_Hyps (drop_V j i) P (Strengthen_Hyps j h)).

Definition
    n_admis_strengthen : (h:Hyps)(n:N)(Q:F)(N_Deduc h n Q)->Prop :=
	[h:Hyps][n:N][Q:F][D:(N_Deduc h n Q)]
	 (i:nat)
	  ~(Occurs_In_N i n)->
	   (N_Deduc (Strengthen_Hyps i h) (drop_N i n) Q).

Definition
    a_admis_strengthen : (h:Hyps)(a:A)(Q:F)(A_Deduc h a Q)->Prop :=
	[h:Hyps][a:A][Q:F][D:(A_Deduc h a Q)]
	 (i:nat)
	  ~(Occurs_In_A i a)->
	   (A_Deduc (Strengthen_Hyps i h) (drop_A i a) Q).

Lemma N_admis_strengthen :
	((h:Hyps)(n:N)(Q:F)(n0:(N_Deduc h n Q))
	 (n_admis_strengthen h n Q n0))/\
	 ((h:Hyps)(a:A)(Q:F)(a0:(A_Deduc h a Q))
	  (a_admis_strengthen h a Q a0)).

Lemma N_Admis_Strengthen :
	(h:Hyps)(n:N)(Q:F)(i:nat)
	 (N_Deduc h n Q)->
	  ~(Occurs_In_N i n)->
	   (N_Deduc (Strengthen_Hyps i h) (drop_N i n) Q).

Lemma A_Admis_Strengthen :
	(h:Hyps)(a:A)(Q:F)(i:nat)
	 (A_Deduc h a Q)->
	  ~(Occurs_In_A i a)->
	   (A_Deduc (Strengthen_Hyps i h) (drop_A i a) Q).

Definition l_admis_strengthen : (h:Hyps)(l:L)(Q:F)(L_Deriv h l Q)->Prop :=
	[h:Hyps][l:L][Q:F][l0:(L_Deriv h l Q)]
	 (i:nat)
	   ~(Occurs_In_L i l)->
	    (L_Deriv (Strengthen_Hyps i h) (drop_L i l) Q).

Lemma L_admis_strengthen : (h:Hyps)(l:L)(Q:F)(l0:(L_Deriv h l Q))
			(l_admis_strengthen h l Q l0).

Lemma L_Admis_Strengthen :
	(h:Hyps)(l:L)(Q:F)(i:nat)
	 (L_Deriv h l Q)->
	   ~(Occurs_In_L i l)->
	    (L_Deriv (Strengthen_Hyps i h) (drop_L i l) Q).

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

Lemma Hyps_ref_eq :
	(i,j:V)(P,Q:F)(h:Hyps)
	 i=j->
	  (In_Hyps i P h)->
	   (In_Hyps j Q h)->
	    P=Q.

Lemma V_Exch_S_Bridge :
	(i,j:nat)
	 (V_Exchange (S i) (S j))=
	  (S (V_Exchange i j)).

Lemma V_Exch_id :
	(i:nat)
	 (V_Exchange i i)=(S i).

Lemma In_Exch1 :
	(h:Hyps)(i,j:nat)(P:F)
	 (lt i j)->
	  (In_Hyps i P h)->
	   (In_Hyps i P (Hyps_Exchange j h)).

Lemma In_Exch2 :
	(h:Hyps)(i,j:nat)(P:F)
	 (lt (S j) i)->
	  (In_Hyps i P h)->
	   (In_Hyps i P (Hyps_Exchange j h)).

Lemma In_Exch :
	(i,j:nat)(h:Hyps)(P,Q,R:F)
	 (In_Hyps i P h)->
	  (In_Hyps j Q h)->
	   (In_Hyps (S j) R h)->
	    (In_Hyps (V_Exchange j i) P (Hyps_Exchange j h)).

Definition l_admis_exch1 :
	(h:Hyps)(l:L)(R:F)(L_Deriv h l R)->Prop :=
	 [h:Hyps][l:L][R:F][l0:(L_Deriv h l R)](j:nat)(P,Q:F)
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (L_Deriv (Hyps_Exchange j h)
		     (L_Exchange j l)
		     R).

Lemma L_admis_exch : 
	(h:Hyps)(l:L)(R:F)(D:(L_Deriv h l R))
	 (l_admis_exch1 h l R D).

Lemma L_Admis_Exch :
	(h:Hyps)(l:L)(R:F)(j:nat)(P,Q:F)
	 (L_Deriv h l R)->
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (L_Deriv (Hyps_Exchange j h)
		     (L_Exchange j l)
		     R).

Lemma Hyps_Exchange_Top :
	(P,Q:F)(h:Hyps)
	 (Hyps_Exchange O (Add_Hyp P (Add_Hyp Q h)))=
	  (Add_Hyp Q (Add_Hyp P h)).

Lemma L_Admis_Exch_Top :
	(P,Q,R:F)(h:Hyps)(l:L)
	 (L_Deriv (Add_Hyp P (Add_Hyp Q h)) l R)->
	  (L_Deriv (Add_Hyp Q (Add_Hyp P h)) (L_Exchange O l) R).

Definition n_admis_exch :
	(h:Hyps)(n:N)(R:F)(N_Deduc h n R)->Prop :=
	 [h:Hyps][n:N][R:F][n0:(N_Deduc h n R)](j:nat)(P,Q:F)
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (N_Deduc (Hyps_Exchange j h)
		     (N_Exchange j n)
		     R).

Definition a_admis_exch :
	(h:Hyps)(a:A)(R:F)(A_Deduc h a R)->Prop :=
	 [h:Hyps][a:A][R:F][a0:(A_Deduc h a R)](j:nat)(P,Q:F)
	  (In_Hyps j P h)->
	   (In_Hyps (S j) Q h)->
	    (A_Deduc (Hyps_Exchange j h)
		     (A_Exchange j a)
		     R).

Lemma N_admis_exch :
	((h:Hyps)(n:N)(R:F)(n0:(N_Deduc h n R))(n_admis_exch h n R n0))/\
	 ((h:Hyps)(a:A)(R:F)(a0:(A_Deduc h a R))(a_admis_exch h a R a0)).

Lemma N_Admis_Exch : (h:Hyps)(n:N)(R:F)(j:nat)(P,Q:F)
	(N_Deduc h n R)->
	 (In_Hyps j P h)->
	  (In_Hyps (S j) Q h)->
	   (N_Deduc (Hyps_Exchange j h)
		    (N_Exchange j n)
		    R).

Lemma A_Admis_Exch : (h:Hyps)(a:A)(R:F)(j:nat)(P,Q:F)
	(A_Deduc h a R)->
	 (In_Hyps j P h)->
	  (In_Hyps (S j) Q h)->
	   (A_Deduc (Hyps_Exchange j h)
		    (A_Exchange j a)
		    R).

Lemma V_Exchange_inv :
	(x:V)(i,j:nat)
	 i=j->
	  (V_Exchange i (V_Exchange j x))=x.

Lemma L_Exchange_inv :
	(l:L)(i,j:nat)
	 i=j->
	  (L_Exchange i (L_Exchange j l))=l.

Lemma M_Admis_Weaken :
	(h:Hyps)(m:M)(P:F)(j:nat)(Q:F)
	 (M_Deriv h m P)->
	  (lt j (S (Len_Hyps h)))->
	   (M_Deriv (Weaken_Hyps j Q h) (lift_M j m) P).

Lemma Ms_Admis_Weaken :
	(ms:Ms)(h:Hyps)(R:F)(P:F)(j:nat)(Q:F)
	 (Ms_Deriv h R ms P)->
	  (lt j (S (Len_Hyps h)))->
	   (Ms_Deriv (Weaken_Hyps j Q h) R (lift_Ms j ms) P).

Lemma M_Admis_Weaken_Top :
	(h:Hyps)(m:M)(P:F)
	 (M_Deriv h m P)->
	  (Q:F)(M_Deriv (Add_Hyp Q h) (lift_M O m) P).

Lemma Ms_Admis_Weaken_Top :
	(ms:Ms)(h:Hyps)(R,P:F)
	 (Ms_Deriv h R ms P)->
	  (Q:F)(Ms_Deriv (Add_Hyp Q h) R (lift_Ms O ms) P).

Lemma N_Admis_Weaken_Top :
	(h:Hyps)(n:N)(P:F)
	 (N_Deduc h n P)->
	  (Q:F)(N_Deduc (Add_Hyp Q h) (lift_N O n) P).

Lemma A_Admis_Weaken_Top :
	(h:Hyps)(a:A)(P:F)
	 (A_Deduc h a P)->
	  (Q:F)(A_Deduc (Add_Hyp Q h) (lift_A O a) P).

Lemma L_Admis_Weaken_Top :
	(h:Hyps)(l:L)(P:F)
	 (L_Deriv h l P)->
	  (Q:F)(L_Deriv (Add_Hyp Q h) (lift_L O l) P).

Definition lift_rhobar_bridge : M->Prop :=
	[m:M](i:nat)
	 (lift_L i (rhobar m))=
	  (rhobar (lift_M i m)).

Definition lift_rhobar1_bridge : Ms->Prop :=
	[ms:Ms](i,j:nat)(m:M)
	 (lt O i)->
	  ((m1:M)(k:nat)
	    (lt (Height_M m1) (Height_Ms (mcons m ms)))->
	     (lift_L k (rhobar m1))=
	      (rhobar (lift_M k m1)))->
	   (rhobar1 i (lift_Ms j (mcons m ms)))=
	    (lift_L (plus i j) (rhobar1 i (mcons m ms))).

Lemma lift_rhobar_Bridge :
	((m:M)(lift_rhobar_bridge m))/\
	 ((ms:Ms)(lift_rhobar1_bridge ms)).

Lemma Lift_RhoBar_Bridge :
	(m:M)(i:nat)
	 (lift_L i (rhobar m))=
	  (rhobar (lift_M i m)).

Lemma Lift_RhoBar1_Bridge :
	(ms:Ms)(i,j:nat)(m:M)
	 (lt O i)->
	  (rhobar1 i (lift_Ms j (mcons m ms)))=
	    (lift_L (plus i j) (rhobar1 i (mcons m ms))).

Lemma Lifts_RhoBar_Bridge :
	(i,j:nat)(m:M)
	 (lifts_L i j (rhobar m))=
	  (rhobar (lifts_M i j m)).

Lemma Lift_RhoBar1_Bridge1 :
	(ms:Ms)(i,j:nat)
	 (lt O i)->
	  (rhobar1 i (lift_Ms j ms))=
	    (lift_L (plus i j) (rhobar1 i ms)).

Lemma RhoBar1_Lifts_Ms1 :
	(ms:Ms)(i,j:nat)
	 (rhobar1 j (lifts_Ms (S i) O ms))=
	  (rhobar1 (S j) (lifts_Ms i O ms)).

Lemma RhoBar1_Lifts_Ms :
	(i,j:nat)(ms:Ms)
	 (rhobar1 j (lifts_Ms i O ms))=
	  (rhobar1 (plus j i) ms).

Definition rhobar21 : M->Prop :=
	[m:M](x:V)(ms:Ms)
	 ((ms1:Ms)(i:nat)
	   (lt (Height_Ms ms1) (Height_Ms (mcons m ms)))->
	    (rhobar1 (S i) ms1)=
	     (rhobar (sc O (lifts_Ms (S i) O ms1))))->
	  (rhobar (sc x (mcons m ms)))=
	   (app x (rhobar m) (rhobar (sc O (lift_Ms O ms)))).

Definition rhobar22 : Ms->Prop :=
	[ms:Ms](i:nat)
	 (rhobar1 (S i) ms)=
	  (rhobar (sc O (lifts_Ms (S i) O ms))).

Lemma Rhobar21 :
	((m:M)(rhobar21 m))/\
	 ((ms:Ms)(rhobar22 ms)).

Lemma RhoBar1 : (x:V)
	(rhobar (sc x mnil))=(vr x).

Lemma RhoBar2 : (ms:Ms)(x:V)(m:M)
	(rhobar (sc x (mcons m ms)))=
	 (app x (rhobar m) (rhobar (sc O (lift_Ms O ms)))).

Lemma RhoBar3 : (m:M)
	(rhobar (lambda m))=(lm (rhobar m)).

Definition l_admis_rhobar_m : M->Prop :=
	[m:M](h:Hyps)(P:F)
	 (M_Deriv h m P)->
	  (L_Deriv h (rhobar m) P).

Definition l_admis_rhobar_ms : Ms->Prop :=
	[ms:Ms](h:Hyps)(P,Q:F)
	 ((m1:M)(h1:Hyps)(P1:F)
	   (lt (Height_M m1) (Height_Ms ms))->
	    (M_Deriv h1 m1 P1)->
	     (L_Deriv h1 (rhobar m1) P1))->
	  (Ms_Deriv (Add_Hyp Q h) Q ms P)->
	   (L_Deriv (Add_Hyp Q h) (rhobar (sc O ms)) P).

Lemma L_Admis_RhoBar1 :
	((m:M)(l_admis_rhobar_m m))/\
	 ((ms:Ms)(l_admis_rhobar_ms ms)).

Lemma L_Admis_RhoBar : (h:Hyps)(m:M)(P:F)
	(M_Deriv h m P)->
	 (L_Deriv h (rhobar m) P).

Lemma L_Admis_Rho : (h:Hyps)(n:N)(P:F)
	(N_Deduc h n P)->
	 (L_Deriv h (rho n) P).

Definition
    n_admis_sub :
	(h:Hyps)(n:N)(P:F)(N_Deduc h n P)->Prop :=
	 [h:Hyps][n:N][P:F][D:(N_Deduc h n P)]
	  (g:nat)(Q:F)(a0:A)
	   (In_Hyps g Q h)->
	     (A_Deduc (Strengthen_Hyps g h) a0 Q)->
	      (N_Deduc (Strengthen_Hyps g h)
		       (NsubstAV a0 g n)
		       P).

Definition
    a_admis_sub :
	(h:Hyps)(a:A)(P:F)(A_Deduc h a P)->Prop :=
	 [h:Hyps][a:A][P:F][D:(A_Deduc h a P)]
	 (g:nat)(Q:F)(a0:A)
	  (In_Hyps g Q h)->
	    (A_Deduc (Strengthen_Hyps g h) a0 Q)->
	     (A_Deduc (Strengthen_Hyps g h)
		      (AsubstAV a0 g a)
		      P).

Lemma N_admis_sub :
	((h:Hyps)(n:N)(P:F)(D:(N_Deduc h n P))(n_admis_sub h n P D))/\
	 ((h:Hyps)(a:A)(P:F)(D:(A_Deduc h a P))(a_admis_sub h a P D)).

Lemma N_Admis_Sub :
	(h:Hyps)(n:N)(P:F)(Q:F)(a0:A)(g:nat)
	 (N_Deduc h n P)->
	  (In_Hyps g Q h)->
	    (A_Deduc (Strengthen_Hyps g h) a0 Q)->
	     (N_Deduc (Strengthen_Hyps g h)
		      (NsubstAV a0 g n)
		      P).

Lemma A_Admis_Sub :
	(h:Hyps)(a:A)(P:F)(Q:F)(a0:A)(g:nat)
	 (A_Deduc h a P)->

	  (In_Hyps g Q h)->
	    (A_Deduc (Strengthen_Hyps g h) a0 Q)->
	     (A_Deduc (Strengthen_Hyps g h) 
		      (AsubstAV a0 g a)
		      P).

Lemma SW_Id :
	(h:Hyps)(i:nat)(P:F)
	 (Strengthen_Hyps i (Weaken_Hyps i P h))=
	  h.

Definition n_admis_phi : (h:Hyps)(l:L)(P:F)(L_Deriv h l P)->Prop :=
[h:Hyps][l:L][P:F][l0:(L_Deriv h l P)](N_Deduc h (phi l) P).

Lemma N_Admis_Phi_1 : (h:Hyps)(l:L)(P:F)(l0:(L_Deriv h l P))
		(n_admis_phi h l P l0).

Lemma N_Admis_Phi : (h:Hyps)(l:L)(P:F)
	(L_Deriv h l P)->
	 (N_Deduc h (phi l) P).

Lemma M_Admis_PhiBar : (h:Hyps)(l:L)(P:F)
	(L_Deriv h l P)->
	 (M_Deriv h (phibar l) P).

Lemma Exchange_Lift_V :
	(v,x,y:V)
	 (x=y)->
	  (V_Exchange x (lift_V y v))=
	   (lift_V (S y) v).

Definition exchange_lift_m : M->Prop :=
	[m:M](x,y:V)
	 x=y->
	  (M_Exchange x (lift_M y m))=
	   (lift_M (S y) m).

Definition exchange_lift_ms : Ms->Prop :=
	[ms:Ms](x,y:V)
	 x=y->
	  (Ms_Exchange x (lift_Ms y ms))=
	   (lift_Ms (S y) ms).

Lemma Exchange_lift_m :
	((m:M)(exchange_lift_m m))/\
	 ((ms:Ms)(exchange_lift_ms ms)).

Lemma Exchange_Lift_M :
	(x,y:V)(m:M)
	 x=y->
	  (M_Exchange x (lift_M y m))=
	   (lift_M (S y) m).

Lemma Exchange_Lift_Ms :
	(x,y:V)(ms:Ms)
	 x=y->
	  (Ms_Exchange x (lift_Ms y ms))=
	   (lift_Ms (S y) ms).

Lemma Lift_Exchange_V1 :
	(v,x,y:V)
	 (lt x (S y))->
	  (lift_V x (V_Exchange y v))=
	   (V_Exchange (S y) (lift_V x v)).

Definition lift_exchange_m1 : M->Prop :=
	[m:M](x,y:nat)
	 (lt x (S y))->
	  (lift_M x (M_Exchange y m))=
	   (M_Exchange (S y) (lift_M x m)).

Definition lift_exchange_ms1 : Ms->Prop :=
	[ms:Ms](x,y:nat)
	 (lt x (S y))->
	  (lift_Ms x (Ms_Exchange y ms))=
	   (Ms_Exchange (S y) (lift_Ms x ms)).

Lemma lift_exchange_M1 :
	((m:M)(lift_exchange_m1 m))/\
	 ((ms:Ms)(lift_exchange_ms1 ms)).

Lemma Lift_Exchange_M1 :
	(m:M)(x,y:nat)
	 (lt x (S y))->
	  (lift_M x (M_Exchange y m))=
	   (M_Exchange (S y) (lift_M x m)).

Lemma Lift_Exchange_Ms1 :
	(ms:Ms)(x,y:nat)
	 (lt x (S y))->
	  (lift_Ms x (Ms_Exchange y ms))=
	   (Ms_Exchange (S y) (lift_Ms x ms)).

Definition exchange_rhobar_bridge : M->Prop :=
	[m:M](x:V)
	 (L_Exchange x (rhobar m))=
	  (rhobar (M_Exchange x m)).

Definition exchange_rhobar1_bridge : Ms->Prop :=
	[ms:Ms](x,y:V)
	 (L_Exchange x (rhobar (sc y ms)))=
	  (rhobar (M_Exchange x (sc y ms))).

Lemma Exchange_rhobar_bridge :
	((m:M)(exchange_rhobar_bridge m))/\
	 ((ms:Ms)(exchange_rhobar1_bridge ms)).

Lemma Exchange_RhoBar_Bridge :
	(x:nat)(m:M)
	 (L_Exchange x (rhobar m))=
	  (rhobar (M_Exchange x m)).

Definition height_m_exchange : M->Prop :=
	[m:M](x:nat)
	 (Height_M (M_Exchange x m))=
	  (Height_M m).

Definition height_ms_exchange : Ms->Prop :=
	[ms:Ms](x:nat)
	 (Height_Ms (Ms_Exchange x ms))=
	  (Height_Ms ms).

Lemma Height_m_exchange :
	((m:M)(height_m_exchange m))/\
	 ((ms:Ms)(height_ms_exchange ms)).

Lemma Height_M_Exchange :
	(m:M)(x:nat)
	 (Height_M (M_Exchange x m))=
	  (Height_M m).

Lemma Height_Ms_Exchange :
	(ms:Ms)(x:nat)
	 (Height_Ms (Ms_Exchange x ms))=
	  (Height_Ms ms).

Definition msub_exch_bridge1 : M->Prop :=
	[m:M](x,y:V)(m1:M)
	 (MsubstVMV x m1 y (M_Exchange y m))=
	  (MsubstVMV x m1 (S y) m).

Definition mssub_exch_bridge1 : Ms->Prop :=
	[ms:Ms](x,y:V)(m1:M)
	 (MssubstVMV x m1 y (Ms_Exchange y ms))=
	  (MssubstVMV x m1 (S y) ms).

Lemma Msub_exch_bridge1 :
	((m:M)(msub_exch_bridge1 m))/\
	 ((ms:Ms)(mssub_exch_bridge1 ms)).

Lemma Msub_Exch_Bridge1 :
	 (m:M)(x,y:V)(m1:M)
	 (MsubstVMV x m1 y (M_Exchange y m))=
	  (MsubstVMV x m1 (S y) m).

Lemma Mssub_Exch_Bridge1 :
	(ms:Ms)(x,y:V)(m1:M)
	 (MssubstVMV x m1 y (Ms_Exchange y ms))=
	  (MssubstVMV x m1 (S y) ms).

Mutual Inductive
    Norm_L : L->Prop :=
	norm_vr : (x:V)(Norm_L (vr x)) |
	norm_app :
		(x:V)(l1,l2:L)
		 (Norm_L l1)->
		  (Norm'_L l2)->
		   (Norm_L (app x l1 l2)) |
	norm_lm :
		(l:L)
		 (Norm_L l)->
		  (Norm_L (lm l))
with
    Norm'_L : L->Prop :=
	norm'_vr : (Norm'_L (vr O)) |
	norm'_app :
		(l1,l2:L)
		 (Norm_L l1)->
		  (Norm'_L l2)->
		   ~(Occurs_In_L O l1)->
		    ~(Occurs_In_L (S O) l2)->
		     (Norm'_L (app O l1 l2)).

Scheme Norm_Norm'_L_ind1 := Induction for Norm_L Sort Prop
  with Norm'_Norm_L_ind1 := Induction for Norm'_L Sort Prop.

Lemma Norm_Norm'_L_ind :
	(P:(l:L)(Norm_L l)->Prop)
        (P0:(l:L)(Norm'_L l)->Prop)
         ((x:V)(P (vr x) (norm_vr x)))
          ->((x:V)
              (l1,l2:L)
               (n:(Norm_L l1))
                (P l1 n)
                 ->(n0:(Norm'_L l2))
                    (P0 l2 n0)
                     ->(P (app x l1 l2) (norm_app x l1 l2 n n0)))
             ->((l:L)(n:(Norm_L l))(P l n)->(P (lm l) (norm_lm l n)))
                ->(P0 (vr O) norm'_vr)
                   ->((l1,l2:L)
                       (n:(Norm_L l1))
                        (P l1 n)
                         ->(n0:(Norm'_L l2))
                            (P0 l2 n0)
                             ->(n1:~(Occurs_In_L O l1))
                                (n2:~(Occurs_In_L (S O) l2))
                                 (P0 (app O l1 l2)
                                   (norm'_app l1 l2 n n0 n1 n2)))
                      ->((l:L)(n:(Norm_L l))(P l n))/\
			((l:L)(n:(Norm'_L l))(P0 l n)).

Fixpoint
    Norm_Lb [l:L] : bool :=
	<bool>Case l of
	    (* vr x *)[x:V]
		true
	    (* app x l0 l1 *)[x:V][l0,l1:L]
		(andb (Norm_Lb l0)
		      (Norm'_Lb l1))
	    (* .\ l *)[l:L]
		(Norm_Lb l)
	end with
    Norm'_Lb [l:L] : bool :=
	<bool>Case l of
	    (* vr x *)[x:V]
		(nateqb x O)
	    (* app x l0 l1 *)[x:V][l0,l1:L]
		(andb (nateqb x O)
		(andb (negb (Occurs_In_L1 O l0))
		(andb (negb (Occurs_In_L1 (S O) l1))
		(andb (Norm_Lb l0)
		      (Norm'_Lb l1)))))
	    (* .\ l *)[l:L]
		false
	end.

Lemma NMLB1 :
	(x:V)
	 (Norm_Lb (vr x))=true.

Lemma NMLB2 :
	(x:V)(l0,l1:L)
	 (Norm_Lb (app x l0 l1))=
	 (andb (Norm_Lb l0)
	       (Norm'_Lb l1)).

Lemma NMLB3 :
	(l:L)
	 (Norm_Lb (lm l))=
	  (Norm_Lb l).

Lemma NMLB4 :
	(x:V)
	 (Norm'_Lb (vr x))=
	  (nateqb x O).

Lemma NMLB5 :
	(x:V)(l0,l1:L)
	 (Norm'_Lb (app x l0 l1))=
	 (andb (nateqb x O)
	 (andb (negb (Occurs_In_L1 O l0))
	 (andb (negb (Occurs_In_L1 (S O) l1))
	 (andb (Norm_Lb l0)
	       (Norm'_Lb l1))))).

Lemma NMLB6 :
	(l:L)
	 (Norm'_Lb (lm l))=
	  false.

Lemma nmlb1_is_nmlb1 :
	(l:L)
	 ((Norm_L l)->
	  (Norm_Lb l)=true)/\
	 ((Norm'_L l)->
	  (Norm'_Lb l)=true).

Lemma NMLB1_is_NMLB1 :
	(l:L)
	 ((Norm_L l)->
	  (Norm_Lb l)=true).

Lemma NM'LB1_is_NM'LB1 :
	(l:L)
	 ((Norm'_L l)->
	  (Norm'_Lb l)=true).

Lemma nmlb1_is_nmlb2 :
	(l:L)
	 ((Norm_Lb l)=true->
	  (Norm_L l))/\
	 ((Norm'_Lb l)=true->
	  (Norm'_L l)).

Lemma NMLB1_is_NMLB2 :
	(l:L)
	 ((Norm_Lb l)=true->
	  (Norm_L l)).

Lemma NM'LB1_is_NM'LB2 :
	(l:L)
	 ((Norm'_Lb l)=true->
	  (Norm'_L l)).

Lemma NMLB1_is_NMLB3 :
	(l:L)
	 (~(Norm_L l)->
	  (Norm_Lb l)=false).

Lemma NM'LB1_is_NM'LB3 :
	(l:L)
	 (~(Norm'_L l)->
	  (Norm'_Lb l)=false).

Lemma NMLB1_is_NMLB4 :
	(l:L)
	 ((Norm_Lb l)=false->
	  ~(Norm_L l)).

Lemma NM'LB1_is_NM'LB4 :
	(l:L)
	 ((Norm'_Lb l)=false->
	  ~(Norm'_L l)).

Definition NML_compare : L->Prop :=
	[l:L]
	 ((Norm_L l)\/~(Norm_L l)).

Lemma NML_dec : (l:L)(NML_compare l).

Definition NM'L_compare : L->Prop :=
	[l:L]
	 ((Norm'_L l)\/~(Norm'_L l)).

Lemma NM'L_dec : (l:L)(NM'L_compare l).

Definition noi_rhobar1 : M->Prop :=
	[m:M](i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (lift_M i (lift_M i m)))).

Definition noi_rhobar2 : Ms->Prop :=
	[ms:Ms](i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (sc O (lift_Ms i (lift_Ms i ms))))).

Lemma noi_rhobar :
	((m:M)(noi_rhobar1 m))/\
	 ((ms:Ms)(noi_rhobar2 ms)).

Lemma NOI_RhoBar1 :
	(m:M)(i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (lift_M i (lift_M i m)))).

Lemma NOI_RhoBar2 :
	(ms:Ms)(i:nat)
	 ~(Occurs_In_L (S i)
	  (rhobar (sc O (lift_Ms i (lift_Ms i ms))))).

Definition norm_l_rhobar_m : M->Prop :=
	[m:M](Norm_L (rhobar m)).

Definition norm_l_rhobar_ms : Ms->Prop :=
	[ms:Ms]
	  (Norm'_L (rhobar (sc O (lift_Ms O ms)))).

Lemma norm_l_rhobar :
	((m:M)(norm_l_rhobar_m m))/\
	 ((ms:Ms)(norm_l_rhobar_ms ms)).

Lemma Norm_L_RhoBar : (m:M)
	(Norm_L (rhobar m)).

Lemma Norm'_L_RhoBar : (ms:Ms)
	(Norm'_L (rhobar (sc O (lift_Ms O ms)))).

(*
Recursive Definition
    HV_L : L->V :=
	(vr x) => x |
	(app x l1 l2) => 
		(Setifb V
			(nateqb O (HV_L l2))
			x
			(HV_L l2)) |
	(lm l) => (HV_L l).
*)

Inductive
    L_Perm1 : L->L->Prop :=
	l_perm1_lm :
		(l1,l2:L)
		   (L_Perm1 l1 l2)->
		    (L_Perm1 (lm l1) (lm l2)) |
 	l_perm1_app1 :
		(i:V)(l11,l12,l2:L)
		   (L_Perm1 l11 l12)->
		     (L_Perm1 (app i l11 l2) (app i l12 l2)) |
 	l_perm1_app2 :
		(i:V)(l1,l21,l22:L)
		    (L_Perm1 l21 l22)->
		      (L_Perm1 (app i l1 l21) (app i l1 l22)) |
 	l_perm1_app_wkn :
		(x:V)(l1,l2:L)
		 ~(Occurs_In_L O l2)->
		  (L_Perm1 (app x l1 l2) (drop_L O l2)) |
	l_perm1_app_app1 :
		(x,y:V)(l1,l2,l3:L)
		 ((Occurs_In_L O l2)\/(Occurs_In_L (S O) l3))->
		  (Norm'_L l3)->
		   (L_Perm1 (app x l1 (app (S y) l2 l3))
			    (app y
				 (app x l1 l2)
				 (app (lift_V O x)
				      (lift_L O l1)
				      (L_Exchange O l3)))) |
 	l_perm1_app_app2 :
		(x:V)(l1,l2,l3:L)
		 ((Occurs_In_L O l2)\/(Occurs_In_L (S O) l3))->
		  (Norm'_L l3)->
		   (L_Perm1 (app x l1 (app O l2 l3))
			    (app x
				 l1
				 (app O
				      (app (lift_V O x)
					   (lift_L O l1)
					   (lift_L (S O) l2))
				      (app (lifts_V (S (S O)) O x)
					   (lifts_L (S (S O)) O l1)
					   (L_Exchange O
					     (lift_L (S (S O)) l3)))))) |
	l_perm1_app_lm : (x:V)(l1,l2:L)
		    (L_Perm1 (app x l1 (lm l2))
			     (lm (app (lift_V O x)
				      (lift_L O l1)
				      (L_Exchange O l2)))).

Scheme L_Perm1_ind1 := Induction for L_Perm1 Sort Prop.

Lemma perm_not_norm_l1 :
	(l0,l1,l2:L)(x:V)
	 (Occurs_In_L O l1)->
	  ~(Norm_L (app x l0 (app O l1 l2))).

Lemma perm_not_norm_l2 :
	(l0,l1,l2:L)(x:V)
	 (Occurs_In_L (S O) l2)->
	  ~(Norm_L (app x l0 (app O l1 l2))).

Lemma Norm'_Norm_L :
	(l:L)
	 (Norm'_L l)->
	  (Norm_L l).

Lemma Perm_not_norm_l : 
	(l0,l1:L)
	 (L_Perm1 l0 l1)->
	  ~(Norm_L l0).

Lemma Perm_Not_Norm_L :
	(l0,l1:L)
	 (L_Perm1 l0 l1)->
	  ~(Norm_L l0).

Lemma Norm_Imperm_L :
	(l0,l1:L)
	 (Norm_L l0)->
	  ~(L_Perm1 l0 l1).

Inductive
    L_Permn : L->L->Prop :=
	l_permn_base :
	    (l0,l1:L)
	       l0=l1->
	        (L_Permn l0 l1) |
	l_permn_rec :
	    (l0,l1,l2:L)
	     (L_Perm1 l0 l1)->
	      (L_Permn l1 l2)->
	       (L_Permn l0 l2).

Scheme L_Permn_ind1 := Induction for L_Permn Sort Prop.

Definition l_admis_perm1 :
	(l,l0:L)(L_Perm1 l l0)->Prop :=
	 [l,l0:L][d:(L_Perm1 l l0)]
	   (h:Hyps)(P:F)(L_Deriv h l P)->
	    (L_Deriv h l0 P).

Lemma L_admis_perm1 :
	(l,l0:L)(D:(L_Perm1 l l0))
	 (l_admis_perm1 l l0 D).

Lemma L_Admis_Perm1 :
	(l,l0:L)(h:Hyps)(P:F)
	 (L_Perm1 l l0)->
	  (L_Deriv h l P)->
	   (L_Deriv h l0 P).

Lemma L_Perm1n :
	(l,l0:L)
	 (L_Perm1 l l0)->
	  (L_Permn l l0).

Definition l_permnn : (l,l0:L)(L_Permn l l0)->Prop :=
	[l,l0:L][d:(L_Permn l l0)]
	 (l1:L)
	  (L_Permn l0 l1)->
	   (L_Permn l l1).

Lemma L_permnn :
	(l,l0:L)(d:(L_Permn l l0))
	 (l_permnn l l0 d).

Lemma L_Permnn :
	(l,l0,l1:L)
	 (L_Permn l l0)->
	  (L_Permn l0 l1)->
	   (L_Permn l l1).

Definition l_permn_app1 :
	(l,l0:L)(L_Permn l l0)->Prop :=
	 [l,l0:L][D:(L_Permn l l0)]
	  (x:V)(l1:L)
	   (L_Permn (app x l l1) (app x l0 l1)).

Lemma L_permn_app1 :
	(l,l0:L)(D:(L_Permn l l0))
	 (l_permn_app1 l l0 D).

Lemma L_Permn_app1 :
	(l,l0,l1:L)(x:V)
	 (L_Permn l l0)->
	  (L_Permn (app x l l1) (app x l0 l1)).

Definition l_permn_app2 :
	(l0,l1:L)(L_Permn l0 l1)->Prop :=
	 [l0,l1:L][D:(L_Permn l0 l1)]
	  (x:V)(l:L)
	   (L_Permn (app x l l0) (app x l l1)).

Lemma L_permn_app2 :
	(l0,l1:L)(D:(L_Permn l0 l1))
	 (l_permn_app2 l0 l1 D).

Lemma L_Permn_app2 :
	(l,l0,l1:L)(x:V)
	 (L_Permn l0 l1)->
	  (L_Permn (app x l l0) (app x l l1)).

Lemma L_Permn_app :
	(x:V)(l0,l1,l2,l3:L)
	 (L_Permn l0 l1)->
	   (L_Permn l2 l3)->
	    (L_Permn (app x l0 l2) (app x l1 l3)).

Definition l_permn_lm :
	(l0,l1:L)(L_Permn l0 l1)->Prop :=
	 [l0,l1:L][d:(L_Permn l0 l1)]
	    (L_Permn (lm l0) (lm l1)).

Lemma L_permn_lm :
	(l0,l1:L)(d:(L_Permn l0 l1))
	 (l_permn_lm l0 l1 d).

Lemma L_Permn_lm :
	(l,l0:L)
	 (L_Permn l l0)->
	  (L_Permn (lm l) (lm l0)).

Definition l_admis_permn :
	(l,l0:L)(L_Permn l l0)->Prop :=
	 [l,l0:L][d:(L_Permn l l0)]
	  (h:Hyps)(P:F)
	   (L_Deriv h l P)->
	    (L_Deriv h l0 P).

Lemma L_admis_permn :
	(l,l0:L)(d:(L_Permn l l0))
	 (l_admis_permn l l0 d).

Lemma L_Admis_Permn :
	(h:Hyps)(l0,l1:L)(P:F)
	 (L_Permn l0 l1)->
	  (L_Deriv h l0 P)->
	   (L_Deriv h l1 P).

(*
Definition hv_rhobar_m : M->Prop :=
	[m:M](x:V)(l1,l2:L)
	(rhobar m)=(app x l1 l2)->
	 (HV_L l2)=O.

Definition hv_rhobar_ms : Ms->Prop :=
	[ms:Ms]
	 (HV_L (rhobar (sc O ms)))=O.

Lemma HV_rhobar_m :
	((m:M)(hv_rhobar_m m))/\
	 ((ms:Ms)(hv_rhobar_ms ms)).

Apply M_Ms_Height_ind.
(Destruct m; Clear  m).
(Intros x ms; Generalize x ; Case ms; Clear  x ms; Unfold hv_rhobar_m;
 Unfold hv_rhobar_ms; Intros).
(Case H; Clear  H; Intros).
(Simpl in H0; Discriminate H0).

(Generalize H0 ; Clear  H0; Rewrite -> RhoBar2; Intros;
 Injection H0; Clear  H0; Intros).
Rewrite <- H0.
(Case H; Clear  H; Intros).
(Apply H3; Auto).
(Rewrite -> Height_Lift_Ms; Rewrite -> HTM1; Rewrite -> HTM4;
 Rewrite -> sym_max_nat; Apply ltS; Apply lt_max_nat1; Auto).

(Unfold hv_rhobar_m; Unfold hv_rhobar_ms; Intros).
(Simpl in H0; Discriminate H0).

(Destruct ms; Clear  ms; Unfold hv_rhobar_ms; Unfold hv_rhobar_m;
 Intros).
Auto.

Rewrite -> RhoBar2.
Rewrite -> HV_L_eq2.
(Case H; Clear  H; Intros).
(Rewrite -> H; Auto).
(Rewrite -> Height_Lift_Ms; Rewrite -> HTM4; Rewrite -> sym_max_nat;
 Apply lt_max_nat1; Auto).
Save.

Lemma HV_rhobar1 :
	(ms:Ms)
	 (HV_L (rhobar (sc O ms)))=O.

Cut ((m:M)(hv_rhobar_m m))/\((ms:Ms)(hv_rhobar_ms ms)).
(Intros c; Case c; Auto).

Exact HV_rhobar_m.
Save.

Lemma HV_rhobar :
	(m:M)(x:V)(l1,l2:L)
	(rhobar m)=(app x l1 l2)->
	 (HV_L l2)=O.

Cut ((m:M)(hv_rhobar_m m))/\((ms:Ms)(hv_rhobar_ms ms)).
(Intros c; Case c; Auto).

Exact HV_rhobar_m.
Save.
*)

Definition oi_rhobar_m : M->Prop :=
	[m:M](x:V)
	 (Occurs_In_M x m)->
	  (Occurs_In_L x (rhobar m)).

Definition oi_rhobar_ms : Ms->Prop :=
	[ms:Ms](x,y:V)
	 (Occurs_In_Ms x ms)->
	  (Occurs_In_L (S x) (rhobar (sc y (lift_Ms O ms)))).

Lemma oi_rhobar_M :
	((m:M)(oi_rhobar_m m))/\
	 ((ms:Ms)(oi_rhobar_ms ms)).

Lemma OI_RhoBar_M :
	(m:M)(x:V)
	 (Occurs_In_M x m)->
	  (Occurs_In_L x (rhobar m)).

Lemma OI_RhoBar_Ms :
	(ms:Ms)(x,y:V)
	 (Occurs_In_Ms x ms)->
	  (Occurs_In_L (S x) (rhobar (sc y (lift_Ms O ms)))).

Lemma NOI_RhoBar_M :
	(m:M)(x:V)
	 ~(Occurs_In_L x (rhobar m))->
	  ~(Occurs_In_M x m).

Lemma NOI_RhoBar_Ms :
	(ms:Ms)(x:V)
	 ~(Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms))))->
	  ~(Occurs_In_Ms x ms).

Definition oi_rhobar_m1 : M->Prop :=
	[m:M](x:V)
	 (Occurs_In_L x (rhobar m))->
	  (Occurs_In_M x m).

Definition oi_rhobar_ms1 : Ms->Prop :=
	[ms:Ms](x:V)
	 (Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms))))->
	  (Occurs_In_Ms x ms).

Lemma oi_rhobar_M1 :
	((m:M)(oi_rhobar_m1 m))/\
	 ((ms:Ms)(oi_rhobar_ms1 ms)).

Lemma OI_RhoBar_M1 :
	(x:V)(m:M)
	 (Occurs_In_L x (rhobar m))->
	  (Occurs_In_M x m).

Lemma OI_RhoBar_Ms1 :
	(x:V)(ms:Ms)
	 (Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms))))->
	  (Occurs_In_Ms x ms).

Lemma NOI_RhoBar_M1 :
	(x:V)(m:M)
	 ~(Occurs_In_M x m)->
	  ~(Occurs_In_L x (rhobar m)).

Lemma NOI_RhoBar_Ms1 :
	(x:V)(ms:Ms)
	 ~(Occurs_In_Ms x ms)->
	  ~(Occurs_In_L (S x) (rhobar (sc O (lift_Ms O ms)))).

Lemma Drop_RhoBar_Bridge :
	(x:V)(m:M)
	 ~(Occurs_In_M x m)->
	  (drop_L x (rhobar m))=
	   (rhobar (drop_M x m)).

Lemma Drop_Lift_M_Bridge1 :
	(m:M)(i,j:nat)
         ~(Occurs_In_M i m)->
          (lt j (S i))->
           (drop_M (S i) (lift_M j m))=(lift_M j (drop_M i m)).

Lemma Drop_Lift_Ms_Bridge1 :
	(ms:Ms)(i,j:nat)
	 ~(Occurs_In_Ms i ms)->
          (lt j (S i))->
           (drop_Ms (S i) (lift_Ms j ms))=(lift_Ms j (drop_Ms i ms)).

Definition app_red_m : M->Prop :=
	[m:M](x:V)(m1:M)
	  (L_Permn (app x (rhobar m1) (rhobar m))
		   (rhobar (MsubstVMV x m1 O m))).

Definition app_red_ms : Ms->Prop :=
	[ms:Ms](x,y:V)(m1:M)
	  (L_Permn (app x (rhobar m1) (rhobar (sc y ms)))
		   (app x (rhobar m1) (rhobar (sc y ms)))).

Lemma app_red :
	((m:M)(app_red_m m))/\
	 ((ms:Ms)(app_red_ms ms)).

Lemma App_Red_M :
	(x:V)(m1,m:M)
	 (L_Permn (app x (rhobar m1) (rhobar m))
		  (rhobar (MsubstVMV x m1 O m))).

Lemma Norm_Red :
	(l:L)(L_Permn l (rhobar (phibar l))).