proposition: Lemma wef_append : forall u v : Word, wef (Append u v) = Append (wef u) (wef v).
proof: Proof. intros u v. elim u. trivial. unfold wef in |- *. intros x w H. simpl in |- *. rewrite <- H. reflexivity. Qed.
imports: Ensf Words