proposition: Lemma Id_image_G : Id (union X V1) f -> isGram X V1 R1 S1 -> Gim = (X, (V1, (R1, S1))).
proof: Proof. intros Id_u_X_V1_f isG_X_V1_R1_S1. rewrite Gim_egal. rewrite (Id_image_S Id_u_X_V1_f isG_X_V1_R1_S1). rewrite (Id_image_R Id_u_X_V1_f isG_X_V1_R1_S1). rewrite (Id_image_V Id_u_X_V1_f). rewrite (Id_image_X Id_u_X_V1_f). apply refl_equal. Qed.
imports: Ensf Words more_words need fonctions Relations gram