proposition: Lemma Derive_inv3 : forall (R : Ensf) (x y : Word), Derive R x y -> exists A : _, (exists2 w : _, cons A w = x & (exists2 u : _, dans (couple A (word u)) R & (exists2 v : _, cons A v = x & Append u v = y)) \/ (exists2 v : _, Derive R w v & cons A v = y)).
proof: Proof. prolog [ Derive_inv1 Derive Derive_inv2 ] 7. Qed.
imports: Ensf Words more_words need fonctions Relations