proposition: Lemma nil_not_in_l1: ~ In [] L1.
proof: Proof. unfold L1; intros N. Search (In _ (_ >> _)). apply app_in_inv in N. destruct N as (w1, (w2, (H1, (H2, H3)))). apply char_in_inv in H3. subst. destruct w1. + inversion H1. + inversion H1. Qed.
imports: Coq.Lists.List