proposition: Lemma Append_inmonoid_g : forall (X : Ensf) (w1 w2 : Word), inmonoid X (Append w1 w2) -> inmonoid X w1.
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 inmonoid_cons. apply (H w2). apply inmonoid_cons_inv with x; auto. apply inmonoid_cons_inv2 with (Append w w2); auto. Qed.
imports: Ensf