proposition: Lemma Deriveg_Derive : forall (X R : Ensf) (u v : Word), Deriveg X R u v -> Derive R u v.
proof: Proof. intros X R u v Der_g. elim Der_g. intros. apply Derive1; auto. intros. apply Derive2; auto. Qed.
imports: Ensf Words fonctions Relations gram