proposition: Lemma app_l_void_rw: forall (L:language), {} >> L == {}.
proof: Proof. split; intros. - apply app_in_inv in H. destruct H as (w1, (w2, (?, (Ha,Hb)))). apply void_not_in in Ha. contradiction. - apply void_not_in in H. contradiction. Qed.
imports: Coq.Lists.List