proposition: Lemma injproducg_V1 : forall x : Elt, dans x V1 -> injproducg V1 x = injgauche x.
proof: Proof. intros x dans_x_V1. unfold injproducg, extension in |- *. elim (extension_spec V1 injgauche x). intros x0 temp; elim temp; clear temp; intro temp; elim temp; clear temp. auto. intros. absurd (dans x V1); assumption. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4