proposition: Lemma app_l_nil_rw: forall (L:language), Nil >> L == L.
proof: Proof. intros. split; intros. - apply app_in_inv in H. destruct H as (w1, (w2, (?, (Ha, Hb)))). subst. apply nil_in_inv in Ha. subst. assumption. - apply app_in_eq with (w1:=[]) (w2:=w). + apply nil_in. + assumption. Qed.
imports: Coq.Lists.List