Require autocontra.
Require MinMJ_nat.

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).
Induction P.
Induction n.
Induction Q.
Induction n.
Simpl.
Try Trivial.

Intros.
Simpl.
Try Trivial.

Intros.
Simpl.
Try Trivial.

Induction Q.
Induction n.
Simpl.
Try Trivial.

Intros.
Simpl.
Apply nateqb_sym.

Intros.
Simpl.
Try Trivial.

Induction Q.
Simpl.
Try Trivial.

Intros.
Simpl.
Rewrite -> (H f1).
Rewrite -> (H0 f2).
Try Trivial.
Save.

Lemma Feqb_is_eq1 : (P,Q:F)(P=Q)->(Feqb P Q)=true.
Intros.
Rewrite <- H.
Generalize P.
Clear H P Q.
Induction P.
Induction n.
Simpl.
Try Trivial.

Simpl.
Try Trivial.

Simpl.
Intros.
Rewrite -> H.
Rewrite -> H0.
Simpl.
Try Trivial.
Save.

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

Induction P.
Induction Q.
Simpl.
Intros.
Cut (eq ? n n0).
(Intros c;Rewrite -> c).
Try Trivial.

Apply (nateqb_is_eq2 n n0 H).

Intros.
Simpl in H1.
Discriminate H1.

Induction Q.
Intros.
Simpl in H1.
Discriminate H1.

Intros.
Cut (eq ? f f1).
Cut (eq ? f0 f2).
Intros.
Rewrite -> H4.
Rewrite -> H5.
Try Trivial.

Simpl in H3.
Apply H0.
(Generalize H3 ;Clear  H3).
Case (Feqb f0 f2).
Auto.

Case (Feqb f f1).
Auto.

Auto.

Apply H.
(Generalize H3 ;Clear  H3;Simpl).
Case (Feqb f f1).
Auto.

Auto.
Save.

Lemma Feqb_is_eq3 : (P,Q:F)(~P=Q)->(Feqb P Q)=false.
Unfold not .
Intros.
Apply bool_dec5.
Unfold not .
Intros.
Apply H.
Apply (Feqb_is_eq2 P Q H0).
Save.

Lemma Feqb_is_eq4 : (P,Q:F)(Feqb P Q)=false->~P=Q.
Intros.
Cut (not (eq ? (Feqb P Q) true)).
Unfold not .
Intros.
Apply H0.
Apply (Feqb_is_eq1 P Q H1).

Apply bool_dec6.
Auto.
Save.

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).
Unfold F_compare1.
Intros.
Case (Feqb P Q).
Left.
Try Trivial.

Right.
Try Trivial.
Save.

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

Lemma Feq_dec : (P,Q:F)(F_compare P Q).
Unfold F_compare .
Intros.
Cut (F_compare1 P Q).
Unfold F_compare1 .
Intros c;Elim c;[Clear  c;Intros c|Clear  c;Intros c].
Left.
Apply (Feqb_is_eq2 P Q c).

Right.
Apply Feqb_is_eq4.
Auto.

Exact (Feqb_dec P Q).
Save.

Lemma Feq_dec1 : (i,j:F)(P:Prop)
		i=j->
		 ~i=j->
		  P.
Intros.
Cut (eq ? (Feqb i j) true).
Rewrite -> (Feqb_is_eq3 i j H0).
(Intros d;Discriminate d).

Exact (Feqb_is_eq1 i j H).
Save.

Lemma Feq_dec2 : (i,j:F)(P:Prop)
		i=j->
		 ~i=j->
		  ~P.
Intros.
Unfold not .
Intros.
Exact (Feq_dec1 i j False H H0).
Save.