proposition: Lemma eqfarray_sym : forall m1 m2 : farray, eq m1 m2 -> eq m2 m1.
proof: Proof. intros (m,Hm,Hd); induction m; intros (m',Hm',Hd'); 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'. apply nodefault_tail in Hd. apply nodefault_tail in Hd'. 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 Hd (Build_farray H1 Hd')); auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance