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