Require MinMJ_rhobar.
Require MinMJ_Bridge2.

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