proposition: Lemma first_point_of_convergence_ugly: forall l1 l2 (v: V), hd_error l1 <> hd_error l2 -> In v l1 -> In v l2 -> exists l1a l2a v' l1b l2b, l1 = l1a++v'::l1b /\ l2 = l2a++v'::l2b /\ (forall u, In u l1a -> ~ In u l2a) /\ (forall u, In u l2a -> ~ In u l1a) /\ l1a <> l2a.
proof: Proof. induction l1; intros. contradiction. destruct l2. contradiction. destruct H0; destruct H1. ++ subst a; subst v0; simpl in H. contradiction. ++ subst a. apply split_list_In in H1. destruct H1 as [lx [ly ?]]. exists nil. exists (v0::lx). exists v. exists l1. exists ly. split. rewrite app_nil_l; auto. split. simpl; rewrite H0; auto. split. intros. contradiction. split. unfold not; intros; auto. unfold not; intros. inversion H1. ++ subst v0. apply split_list_In in H0. destruct H0 as [lx [ly ?]]. exists (a::lx). exists nil. exists v. exists ly. exists l2. split. simpl; rewrite H0; auto. split. apply app_nil_l. split. unfold not; intros. contradiction. split. intros. contradiction. unfold not; intros; inversion H1. ++ assert (a <> v0). unfold not; intros. subst a. simpl in H. contradiction. destruct l1. contradiction. destruct l2. contradiction. destruct (EV v1 v2). ** hnf in e. subst v2. exists (a::nil). exists (v0::nil). exists v1. exists l1. exists l2. split. simpl; auto. split. simpl; auto. split. unfold not; intros. destruct H3. subst a. destruct H4. subst v0. all: try contradiction. split. unfold not; intros. destruct H3. subst v0. destruct H4. subst a. all: try contradiction. unfold not; intros. inversion H3. contradiction. ** unfold complement, equiv in c. apply (IHl1 (v2::l2) v) in H1. 2: { simpl; unfold not; intros; inversion H3. contradiction. } 2: auto. destruct H1 as [l1a [l2a [v' [l1b [l2b [? [? [? ?]]]]]]]]. rename v0 into b. destruct (in_dec EV a l2a). apply split_list_In_first in i. destruct i as [l2a1 [l2a2 [? ?]]]. exists nil. exists (b::l2a1). exists a. exists (v1::l1). exists (l2a2++v'::l2b). split. simpl; auto. split. rewrite H3. subst l2a. simpl. rewrite app_comm_cons. rewrite <- (app_assoc (b::l2a1) (a::l2a2)). simpl. auto. split. unfold not; intros; contradiction. split. unfold not; intros; contradiction. unfold not; intros. inversion H8. destruct (in_dec EV b l1a). apply split_list_In_first in i. destruct i as [l1a1 [l1a2 [? ?]]]. exists (a::l1a1). exists nil. exists b. exists (l1a2++v'::l1b). exists (v2::l2). split. rewrite H1. subst l1a. simpl. rewrite app_comm_cons. rewrite <- (app_assoc (a::l1a1) (b::l1a2)). simpl; auto. split. simpl; auto. split. unfold not; intros; contradiction. split. unfold not; intros; contradiction. unfold not; intros. inversion H8. exists (a::l1a). exists (b::l2a). exists v'. exists l1b. exists l2b. split. simpl. rewrite H1. auto. split. simpl. rewrite H3. auto. split. unfold not; intros. destruct H6; destruct H7. subst a; subst b. contradiction. subst a. contradiction. subst b. contradiction. apply H4 in H6. contradiction. split. unfold not; intros. destruct H6; destruct H7. subst a; subst b. contradiction. subst b. contradiction. subst a. contradiction. apply H5 in H7. contradiction. auto. unfold not; intros. inversion H6. contradiction. Qed.
imports: Coq.Logic.Classical CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext CertiGraph.graph.graph_model CertiGraph.graph.graph_relation CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.FiniteGraph