proposition: Lemma N_dans_S_V1' : ~ dans S' V1'.
proof: Proof. red in |- *. replace V1' with (map injgauche V1). intros. elimtype (exists y : Elt, dans y V1 /\ S' = (fun e : Elt => couple e zero) y). intros x temp; elim temp; clear temp. intros dans_x_V1 S_egal. absurd (S' = couple x zero). unfold S', zero in |- *. discriminate. auto. apply (dans_map (fun e : Elt => couple e zero)). assumption. unfold V1' in |- *. simpl in |- *. auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4