proposition: Lemma compare_Cmp : forall s1 s2, Cmp (compare_pure s1 s2) (R.elements s1) (R.elements s2).
proof: Proof. intros; unfold compare_pure. rewrite <- (app_nil_r (R.elements s1)). replace (R.elements s2) with (P.flatten_e (R.cons s2 (R.End _))) by (rewrite P.cons_1; simpl; rewrite app_nil_r; auto). auto using compare_cont_Cmp, compare_end_Cmp. Qed.
imports: FunInd FMapInterface FMapList ZArith Int