proposition: Lemma eqfarray_refl : forall m : farray, eq m m.
proof: Proof. intros (m,Hm,Hd); induction m; unfold eq; simpl; auto. destruct a. destruct (compare k k) as [Hlt|Heq|Hlt]; auto. apply lt_not_eq in Hlt. auto. split. apply eq_refl. inversion_clear Hm. apply nodefault_tail in Hd. apply (IHm H Hd). apply lt_not_eq in Hlt. auto. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance