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

(Apply M_Ms_Deriv_ind; Unfold n_admis_theta; Unfold n_admis_theta'; Intros).
(Rewrite -> th1; Apply H; Apply A_Axiom; Auto).

(Rewrite -> th2; Apply Implies_I; Auto).

(Simpl; Apply AN_Axiom; Auto).

(Rewrite -> th4; Apply H0; Apply Implies_E with P:=P1; Auto).
Save.

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

Cut ((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)).
(Unfold n_admis_theta; Intros c; Case c; Clear  c; Auto).

Exact N_admis_theta.
Save.

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

Cut ((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)).
(Unfold n_admis_theta'; Intros c; Case c; Clear  c; Intros).
(Apply H0 with R:=R P:=P; Auto).

Exact N_admis_theta.
Save.