proposition: Lemma pregraph_iso_exp_sym: forall `(g: @PreGraph V E EV EE) `(g': @PreGraph V' E' EV' EE') vmap vmap' emap emap', pregraph_isomorphism_explicit g g' vmap vmap' emap emap' -> pregraph_isomorphism_explicit g' g vmap' vmap emap' emap.
proof: Proof. intros. destruct H. split; try assumption. - apply bijective_sym; assumption. - apply bijective_sym; assumption. - intros. destruct edge_bij0. apply evalid_bij_inv0 in H. rewrite <- (surjective e) at 1. rewrite <- src_bij0 by assumption. apply bijective_sym in vertex_bij0. destruct vertex_bij0. rewrite surjective0. reflexivity. - intros. destruct edge_bij0. apply evalid_bij_inv0 in H. rewrite <- (surjective e) at 1. rewrite <- dst_bij0 by assumption. apply bijective_sym in vertex_bij0. destruct vertex_bij0. rewrite surjective0. reflexivity. Qed.
imports: Coq.Lists.List Coq.Program.Basics CertiGraph.lib.Coqlib CertiGraph.graph.graph_model CertiGraph.lib.EquivDec_ext