proposition: Lemma Id_injproducg1 : forall x : Elt, dans x X -> injproducg V1 x = x :>Elt.
proof: Proof. unfold Id, injproducg in |- *. simpl in |- *. intros x dans_x_X. apply extension_out. apply inter_dans with X; auto. Qed.
imports: Ensf Words more_words Rat need fonctions Relations gram gram2 gram3 gram4