proposition: Lemma lang_dotx1 x: lang_dot tt tt tt x (lang_one tt) ≡ x.
proof: Proof. intro w. split. intros [u Hu [v <- ->]]. now rewrite app_nil_r. intro Hw. exists w; trivial. exists nil. reflexivity. now rewrite app_nil_r. Qed.
imports: List prop monoid