proposition: Lemma lp_graph_iso_exp_sym: forall `(g: @LabeledGraph V E EV EE DV DE DG) g' vmap vmap' emap emap', label_preserving_graph_isomorphism_explicit g g' vmap vmap' emap emap' -> label_preserving_graph_isomorphism_explicit g' g vmap' vmap emap' emap.
proof: Proof. intros. destruct H. split. - apply pregraph_iso_exp_sym. assumption. - intros. destruct lp_pregraph_iso0. destruct vertex_bij0. rewrite <- (surjective v) at 1. rewrite <- vlabel_iso0; auto. - intros. destruct lp_pregraph_iso0. destruct edge_bij0. rewrite <- (surjective e) at 1. rewrite <- elabel_iso0; auto. Qed.
imports: Coq.Lists.List Coq.Program.Basics CertiGraph.lib.Coqlib CertiGraph.graph.graph_model CertiGraph.lib.EquivDec_ext