proposition: Lemma equal_eqP : forall a b, equalP a b <-> a = b.
proof: Proof. intros. split; intro H. unfold equalP in H. case_eq (equal a b); intros; rewrite H0 in H. now apply equal_eq. now contradict H. rewrite H. unfold equalP. now rewrite equal_refl. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses ProofIrrelevance