proposition: Lemma car_not_in_l4: ~ In ["c"; "a"; "r"] L4.
proof: Proof. unfold L4. intros N. destruct N as (n, H). destruct n. { apply app_in_inv in H. destruct H as (w1, (w2, (Hs, (Ha, Hb)))). inversion Ha; subst. inversion Hb; subst. inversion Hs. } apply app_in_inv in H. destruct H as (w1, (w2, (Hs, (Ha, Hb)))). apply pow_char_cons_inv in Ha. destruct Ha as (w', (?, ?)). subst. inversion Hs. Qed.
imports: Coq.Lists.List