Require MinMJ_F.
Require PolyList.
Require MinMJ_
(* Syntactic Definition Hyps := (list F). *)

Grammar command command3 :=
	["Hyps"] -> [$0=<<(list F)>>].

(* Syntactic Definition MT := (nil F). *)

Grammar command command3 :=
	["MT"] -> [$0=<<(nil F)>>].

(* Syntactic Definition Add_Hyp := (cons F). *)

Grammar command command3 :=
	["Add_Hyp" command:command($f) command:command($h)] ->
	[$0 = <<(cons F $f $h)>>].

Grammar command command3 :=
	["Len_Hyps" command:command($h)] ->
	[$0 = <<(length F $h)>>].

Lemma Add_Hyp1 :
	(i:Hyps)(P:F)~(Add_Hyp P i)=i.

Recursive Definition
    Hypseqb : Hyps->Hyps->bool :=
	MT MT => true |
	MT (Add_Hyp P' h') => false |
	(Add_Hyp P h) MT => false |
	(Add_Hyp P h) (Add_Hyp P' h') => (andb (Feqb P P') (Hypseqb h h')).

Lemma Hypseqb_sym :
	(i,j:Hyps)(Hypseqb i j)=(Hypseqb j i).

Lemma Hypseqb_is_eq1 :
	(i,j:Hyps)i=j->(Hypseqb i j)=true.

Lemma Hypseqb_is_eq2 :
	(i,j:Hyps)(Hypseqb i j)=true->i=j.

Lemma Hypseqb_is_eq3 :
	(i,j:Hyps)(~i=j)->(Hypseqb i j)=false.

Lemma Hypseqb_is_eq4 :
	(i,j:Hyps)(Hypseqb i j)=false->~i=j.

Definition Hyps_compare1 : Hyps->Hyps->Prop :=
[i,j:Hyps]((Hypseqb i j)=true)\/(Hypseqb i j)=false.

Lemma Hypseqb_dec :
	(i,j:Hyps)(Hyps_compare1 i j).

Definition Hyps_compare :Hyps->Hyps->Prop :=
	[i,j:Hyps]i=j\/~i=j.

Lemma Hypseq_dec :
	(i,j:Hyps)(Hyps_compare i j).