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