proposition: Lemma Derive_inv2 : forall (R : Ensf) (x y : Word), Derive_inv R x y -> exists A : Elt, (exists2 w : Word, cons A w = x & (exists2 u : Word, dans (couple A (word u)) R & (exists2 v : Word, cons A v = x & Append u v = y)) \/ (exists2 v : Word, Derive R w v & cons A v = y)).
proof: Proof. intros R x y. elim x. unfold Derive_inv in |- *. intuition. intros x0 w Hyp_rec. unfold Derive_inv in |- *. exists x0. exists w; trivial. Qed.
imports: Ensf Words more_words need fonctions Relations