proposition: Lemma eqfarray_trans : forall m1 m2 m3 : farray, eq m1 m2 -> eq m2 m3 -> eq m1 m3.
proof: Proof. intros (m1,Hm1,Hd1); induction m1; intros (m2,Hm2,Hd2); destruct m2; intros (m3,Hm3,Hd3); destruct m3; unfold eq; simpl; try destruct a as (x,e); try destruct p as (x',e'); try destruct p0 as (x'',e''); try contradiction; auto. destruct (compare x x') as [Hlt|Heq|Hlt]; destruct (compare x' x'') as [Hlt'|Heq'|Hlt']; try easy. intros; destruct H, H0; subst. case (compare x'' x''); subst; intro HH; try (apply lt_not_eq in HH; now contradict HH). split; auto. inversion_clear Hm1; inversion_clear Hm2; inversion_clear Hm3. apply nodefault_tail in Hd1. apply nodefault_tail in Hd2. apply nodefault_tail in Hd3. apply (IHm1 H Hd1 (Build_farray H3 Hd2) (Build_farray H5 Hd3)); intuition. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance