Require MinMJ_theta.
Require MinMJ_MJ.
Require MinMJ_NJ.

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