proposition: Lemma aabb_in_l4: In ["a"; "a"; "b"; "b"] L4.
proof: Proof. exists 2. apply app_in with (w1:=["a"; "a"]) (w2:=["b"; "b"]). + apply pow_char_cons, pow_char_cons. apply pow_nil. + apply pow_char_cons, pow_char_cons. apply pow_nil. + reflexivity. Qed.
imports: Coq.Lists.List