proposition: Lemma app_r_all_in_skip: forall (L:language) w, In w L -> In w (App L All).
proof: Proof. intros. apply app_in with (w1:=w) (w2:=[]). + assumption. + apply all_in. + rewrite app_nil_r. reflexivity. Qed.
imports: Coq.Lists.List