proposition: Lemma l1_spec: L1 == fun w => exists w', w = w' ++ ["a"].
proof: Proof. unfold L1. unfold Equiv. split; intros. - Search (In _ (_ >> _)). apply app_in_inv in H. destruct H as (wa, (wb, (?, (Ha, Hb)))). subst. unfold In. Search (In _ (Char _ )). apply char_in_inv in Hb. subst. exists wa. reflexivity. - unfold In in H. destruct H as (wa, H). subst. Search (In (_ ++ _) ( _ >> _)). apply app_in_eq. + Search (In _ All). apply all_in. + Search (In _ (Char _)). apply char_in. Qed.
imports: Coq.Lists.List