proposition: Lemma valid_path_si: forall (g1 g2: Gph), structurally_identical g1 g2 -> forall p, valid_path g1 p <-> valid_path g2 p.
proof: Proof. cut (forall g1 g2 : Gph, g1 ~=~ g2 -> forall p : path, valid_path g1 p -> valid_path g2 p). 1: intros; split; apply H; [| symmetry]; auto. intros. destruct p as [v p]. revert v H0. induction p; intros. + destruct H as [? _]. simpl in *. rewrite <- H. auto. + specialize (IHp (dst g1 a)). destruct H0. simpl in H1. split. - destruct H as [_ [? [? _]]]. destruct p; [| destruct H1 as [? _]]; destruct H1 as [? [? ?]]; specialize (H a); rewrite <- H2; intuition. - assert (strong_evalid g1 a -> strong_evalid g2 a). { intros. destruct H2 as [? [? ?]]. destruct H as [? [? [? ?]]]. assert (evalid g2 a) by (rewrite <- H5; auto). specialize (H6 _ H2 H8). specialize (H7 _ H2 H8). rewrite H6, H7 in *. rewrite H in H3, H4. split; auto. } destruct p. 1: simpl; apply H2; auto. destruct H1 as [? ?]. unfold valid_path in IHp. specialize (IHp H3). destruct H3, IHp. simpl. split. 1: apply H2; auto. split. * rewrite <- H5. symmetry. specialize (H2 H1). destruct H1, H2. destruct H as [_ [_ [_ ?]]]. apply H; auto. * apply H6. Qed.
imports: Coq.Logic.ProofIrrelevance Coq.micromega.Lia CertiGraph.lib.Coqlib CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model Coq.Lists.List Coq.Lists.ListDec