proposition: Lemma notequal_neq : forall a b, equal a b = false -> a <> b.
proof: Proof. intros. red. intros. apply not_true_iff_false in H. unfold not in *. intros. apply H. rewrite H0. apply eq_equal. apply eqfarray_refl. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance