proposition: Lemma Append_inmonoid_d : forall (X : Ensf) (w1 w2 : Word), inmonoid X (Append w1 w2) -> inmonoid X w2.
proof: Proof. intros X. simple induction w1. auto. intros x w H w2. replace (Append (cons x w) w2) with (cons x (Append w w2)); auto. intro. apply (H w2). apply inmonoid_cons_inv with x; auto. Qed.
imports: Ensf