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

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.