proposition: Lemma partial_lgraph_elabel_map: forall (t g: UAdjMatGG) l, is_partial_lgraph t g -> incl l (EList t) -> map (elabel t) l = map (elabel g) l.
proof: Proof. induction l; intros. simpl; auto. simpl. replace (elabel g a) with (elabel t a). rewrite IHl; auto. apply incl_cons_inv in H0; destruct H0; auto. apply H. rewrite <- EList_evalid. apply H0. left; auto. Qed.
imports: VST.floyd.proofauto CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.find_lemmas CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.undirected_graph CertiGraph.graph.MathAdjMatGraph