proposition: Lemma map_local_functions_eq: forall (A B: Type) (f f': A -> B) (l: list A), (forall x: A, In x l -> f x = f' x) -> map f l = map f' l.
proof: Proof. induction l; intros. auto. simpl. rewrite (H a). rewrite IHl. auto. intros. apply H. right; auto. left; auto. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist