proposition: Lemma wef_cons : forall (a b : Word) (e : Elt), cons e a = wef b -> exists x : Elt, ex2 (fun w : Word => cons x w = b) (fun w : Word => f x = e /\ wef w = a).
proof: Proof. intros a b e. unfold wef in |- *. case b. simpl in |- *; intro H; discriminate H. simpl in |- *; intros x w H. exists x. exists w. trivial. injection H; auto. Qed.
imports: Ensf Words