proposition: Lemma eqfarray_sym : forall m1 m2 : farray, eq m1 m2 -> eq m2 m1.
proof: Proof. intros (m,Hm); induction m; intros (m', Hm'); destruct m'; unfold eq; simpl; try destruct a as (x,e); try destruct p as (x',e'); auto. destruct (compare x x') as [Hlt|Heq|Hlt]; try easy. inversion_clear Hm; inversion_clear Hm'. intro. destruct H3. subst. case (compare x' x'); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). split; auto. apply (IHm H (Build_slist H1)); auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses