proposition: Lemma Regles_X_V_R : Regles X V R.
proof: Proof. Proof isGram4 X V R S Gram. Hypothesis Mono : is_mono (union X V) f. Lemma inter_Xim_Vim_empty : inter Xim Vim empty. unfold Xim, Vim in |- *; simpl in |- *. red in |- *. split; [ idtac | split ]. auto. auto. intros x dans_x_map_f_X dans_x_map_f_V. elimtype (exists y : Elt, dans y X /\ x = f y :>Elt). elimtype (exists y : Elt, dans y V /\ x = f y :>Elt). intros v temp; elim temp; clear temp. intros dans_v_V x_egal_f_v x_ant temp; elim temp; clear temp. intros dans_x_ant_X x_egal_f_x_ant. elimtype (inter X V empty). intros incl_empty_X temp; elim temp; clear temp. intros incl_empty_V imp. apply dans_empty_imp_P with v. apply imp. replace v with x_ant. assumption. apply Mono. auto. auto. rewrite <- x_egal_f_x_ant; assumption. assumption. exact (isGram2 X V R S Gram). auto. auto. Qed.
imports: Ensf Words more_words need fonctions Relations gram gram2