proposition: Lemma Append_w_nil : forall w : Word, Append w nil = w :>Word.
proof: Proof. simple induction w. auto. intros x w0 H. replace (Append (cons x w0) nil) with (cons x (Append w0 nil)); auto. rewrite H; auto. Qed.
imports: Ensf