proposition: Lemma equal_spec : forall s1 s2 `{Ok s1, Ok s2}, equal s1 s2 = true <-> eq s1 s2.
proof: Proof. unfold equal; intros s1 s2 B1 B2. destruct (@compare_spec s1 s2 B1 B2) as [H|H|H]; split; intros H'; auto; try discriminate. - rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto. - rewrite H' in H. elim (StrictOrder_Irreflexive s2); auto. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat