proposition: Lemma cut1_Append : forall u v : Word, inmonoid X u -> cut1 (Append u v) = Append u (cut1 v).
proof: Proof. intros u v. generalize u; clear u; simple induction u. auto. intros x w Hyp inmon_x_w. replace (cut1 (Append (cons x w) v)) with (cons x (cut1 (Append w v))). replace (Append (cons x w) (cut1 v)) with (cons x (Append w (cut1 v))). apply cons_cons. trivial. apply Hyp. apply inmonoid_cons_inv with x; assumption. trivial. apply sym_equal. unfold Append in |- *. simpl in |- *. apply cut1_cons. apply inmonoid_cons_inv2 with w. trivial. Qed.
imports: Ensf Words more_words need Relations gram gram_g PushdownAutomata