proposition: Lemma l2_spec: L2 == Any >> Any.
proof: Proof. unfold Examples.L2; split; intros. - unfold In in H. destruct w. { inversion H. } destruct w. { inversion H. } destruct w. { Search (App Any _). apply app_l_any_in. apply any_in. } inversion H. - Search (Any >> _). apply app_l_any_in_inv in H. destruct H as (w', (c1, (?, Hi))). subst. apply any_in_inv in Hi. destruct Hi as (c2, ?). subst. reflexivity. Qed.
imports: Coq.Lists.List