proposition: Theorem eq_maps2: forall (A B C: Type) (f : A -> B) (g : C -> B) (la : list A) (lc : list C) defa defc, length la = length lc -> (forall n , n < length la -> f (nth n la defa) = g ( nth n lc defc)) -> map f la = map g lc.
proof: Proof. induction la using rev_list_ind; introv Hleq Hp. invertsn Hleq. symmetry in Hleq. rw length0 in Hleq. subst. reflexivity. allrewrite snoc_as_append. rewrite map_app. rewrite length_app in Hleq. allsimpl. rev_list_dest lc. invertsn Hleq. omega. allrewrite snoc_as_append. rewrite map_app. allsimpl. rewrite length_app in Hleq. allsimpl. assert (length la = length u) as Hleq1 by omega. f_equal. eapply IHla; eauto. intros. assert (n < length (la++[a])) as Hla. rewrite length_app. omega. apply Hp in Hla. rewrite app_nth1 in Hla; auto. rewrite app_nth1 in Hla; auto. eauto. rewrite <- Hleq1; auto. instlemma (Hp (length la)) as Hle. rewrite <- snoc_as_append in Hle. rewrite <- snoc_as_append in Hle. rewrite last_snoc in Hle. rewrite Hleq1 in Hle. rewrite last_snoc in Hle. f_equal; auto. apply Hle. rewrite <- Hleq1. rewrite length_snoc; omega. Qed.
imports: UsefulTypes bin_rels Omega