proposition: Lemma app_exists : forall (s : string) re0 re1, s =~ App re0 re1 <-> exists s0 s1, s = s0 ++ s1 /\ s0 =~ re0 /\ s1 =~ re1.
proof: Proof. intros. split. - intros. inversion H. exists s1, s2. split. * reflexivity. * split. apply H3. apply H4. - intros [ s0 [ s1 [ Happ [ Hmat0 Hmat1 ] ] ] ]. rewrite Happ. apply (MApp s0 _ s1 _ Hmat0 Hmat1). Qed.
imports: Coq(Lia)