proposition: Lemma list_inj_map_NoDup: forall (A B : Type) (f : A -> B) (l : list A), (forall x y : A, In x l -> In y l -> f x = f y -> x = y) -> NoDup l -> NoDup (map f l).
proof: Proof. induction l; intros. simpl. apply NoDup_nil. simpl. apply NoDup_cons. unfold not; intros. apply NoDup_cons_iff in H0; destruct H0. apply list_in_map_inv in H1. destruct H1. destruct H1. apply H in H1. subst a. contradiction. left; auto. right; auto. apply IHl. intros. apply H. right; auto. right; auto. auto. apply NoDup_cons_iff in H0. apply H0. Qed.
imports: VST.floyd.proofauto CertiGraph.graph.graph_model CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.graph.FiniteGraph CertiGraph.kruskal.env_kruskal_edgelist