proposition: Lemma eqfarray_sym : forall m1 m2 : farray, eq m1 m2 -> eq m2 m1.
proof: Proof. unfold eq. intros (m,Hm,d,Hd); induction m; intros (m',Hm',d',Hd'); destruct m'; unfold eq; simpl; destruct (eq_dec d d'); auto; intuition; subst d'; destruct (eq_dec d d) as [He | He]; auto; try destruct a as (x,e); try destruct p as (x',e'); auto; intuition. destruct (compare x x') as [Hlt|Heq|Hlt]; try easy. inversion_clear Hm; inversion_clear Hm'. destruct H. apply nodefault_tail in Hd. apply nodefault_tail in Hd'. subst. case (compare x' x'); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). split; auto. specialize (IHm H0 Hd (Build_slist H2 Hd')). simpl in IHm. case (eq_dec d d) in IHm; intuition. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance