proposition: Lemma expand_01 e: is_01 e -> e ≡ eps e.
proof: Proof. intro H. rewrite (expand e) at 1. rewrite sup_b. apply cupxb. intros. rewrite deriv_01 by assumption. apply dotx0. Qed.
imports: syntax kleene boolean lang lset sums normalisation