proposition: Lemma app_l_char_in: forall c (L:language) w, In w L -> In (c :: w) (App (Char c) L).
proof: Proof. intros. apply app_in with (w1:=[c]) (w2:=w). + apply char_in. + assumption. + reflexivity. Qed.
imports: Coq.Lists.List