proposition: Lemma restriction_transition_d1 : forall (q1 d1 q2 d2 : Ensf) (e1 x e : Elt), dans (couple e1 (couple x e)) (union (injg_d1 q1 d1) (injd_d2 q2 d2)) -> dans e1 (map injgauche q1) -> dans (couple (first e1) (couple x (first e))) d1.
proof: Proof. intros. cut (dans (couple e1 (couple x e)) (injg_d1 q1 d1) \/ dans (couple e1 (couple x e)) (injd_d2 q2 d2)); auto. intro Ht; elim Ht; clear Ht. unfold injg_d1 in |- *. intro. cut (dans (couple e1 (couple x e)) (prodcart (map injgauche q1) (prodcart alph (map injgauche q1))) /\ est_dans_d' d1 (couple e1 (couple x e))). 2: apply dans_tq_imp; auto. intro Ht; elim Ht; clear Ht; intros H2 H3. assumption. unfold injd_d2 in |- *. intro. cut (dans (couple e1 (couple x e)) (prodcart (map injdroite q2) (prodcart alph (map injdroite q2))) /\ est_dans_d' d2 (couple e1 (couple x e))). 2: apply dans_tq_imp; auto. intro Ht; elim Ht; clear Ht; intros H2 H3. cut (dans e1 (map injdroite q2) /\ dans (couple x e) (prodcart alph (map injdroite q2))). 2: apply coupl2; auto. intro Ht; elim Ht; clear Ht; intros H4 H5. absurd (dans e1 (map injdroite q2)); auto. apply absurd_injg_injd with q1; auto. Qed.
imports: Ensf Max Words Dec Reg Rat