proposition: Lemma chemin_A_chemin_2 : forall (q1 qa1 d1 q2 qd2 d2 : Ensf) (e e3 : Elt) (w0 : Word), chemin_A (union_disj q1 q2) (union (pont qa1 qd2) (union (injg_d1 q1 d1) (injd_d2 q2 d2))) e e3 w0 -> dans e (map injdroite q2) -> dans e3 (map injdroite q2) -> chemin (first e) (first e3) q2 d2 w0.
proof: Proof. intros q1 qa1 d1 q2 qd2 d2 e e3 w0 H. elim H; clear H. intros. apply chemin_nil. apply dans_map_injd; auto. apply (f_equal (A:=Elt) (B:=Elt)); auto. intros e1 e0 e2 x w H H0 H1 H2 H3 H4 H5. apply chemin_cons with (first e0); auto. apply H0; auto. cut (dans (couple e1 (couple x e0)) (pont qa1 qd2) \/ dans (couple e1 (couple x e0)) (union (injg_d1 q1 d1) (injd_d2 q2 d2))); auto. intro Ht; elim Ht; clear Ht. intro. cut (x = epsilon :>Elt). 2: apply dans_pont_imp_epsilon with qa1 qd2 e1 e0; auto. intro. absurd (dans x alph); auto. rewrite H7. red in |- *; intro; apply not_dans_epsilon_alph; assumption. intro. cut (dans (couple e1 (couple x e0)) (injg_d1 q1 d1) \/ dans (couple e1 (couple x e0)) (injd_d2 q2 d2)); auto. intro Ht; elim Ht; clear Ht. unfold injg_d1 in |- *. intro. cut (dans (couple e1 (couple x e0)) (prodcart (map injgauche q1) (prodcart alph (map injgauche q1))) /\ est_dans_d' d1 (couple e1 (couple x e0))). 2: apply dans_tq_imp; auto. intro Ht; elim Ht; clear Ht; intros. cut (dans e1 (map injgauche q1) /\ dans (couple x e0) (prodcart alph (map injgauche q1))). 2: apply coupl2; auto. intro Ht; elim Ht; clear Ht; intros. absurd (dans e1 (map injdroite q2)); auto. apply absurd_injg_injd with q1; auto. unfold injd_d2 in |- *. intro. cut (dans (couple e1 (couple x e0)) (prodcart (map injdroite q2) (prodcart alph (map injdroite q2))) /\ est_dans_d' d2 (couple e1 (couple x e0))). 2: apply dans_tq_imp; auto. intro Ht; elim Ht; clear Ht; intros. cut (dans e1 (map injdroite q2) /\ dans (couple x e0) (prodcart alph (map injdroite q2))). 2: apply coupl2; auto. intro Ht; elim Ht; clear Ht; intros. cut (dans x alph /\ dans e0 (map injdroite q2)). 2: apply coupl2; auto. intro Ht; elim Ht; auto. apply dans_map_injd; auto. apply transition_a_droite_2 with q1 qa1 d1 q2 qd2; auto. intros e1 e0 e2 w H H0 H1 H2 H3 H4. cut (dans e1 (map injgauche qa1) /\ dans e0 (map injdroite qd2)). 2: apply transition_dans_pont with q1 d1 q2 d2; auto. intro Ht; elim Ht; clear Ht. intros. absurd (dans e1 (map injdroite q2)); auto. apply absurd_injg_injd with qa1; auto. Qed.
imports: Ensf Max Words Dec Reg Rat