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