proposition: Lemma app_ne : forall (a : ascii) s re0 re1, a :: s =~ (App re0 re1) <-> ([ ] =~ re0 /\ a :: s =~ re1) \/ exists s0 s1, s = s0 ++ s1 /\ a :: s0 =~ re0 /\ s1 =~ re1.
proof: Proof. Admitted. Lemma union_disj : forall (s : string) re0 re1, s =~ Union re0 re1 <-> s =~ re0 \/ s =~ re1. Proof. intros. split. - intros. inversion H. + left. apply H2. + right. apply H1. - intros [ H | H ]. + apply MUnionL. apply H. + apply MUnionR. apply H. Qed.
imports: Coq(Lia)