如何在Coq中证明`A =~ Star re -> B =~ Star re -> A ++ B =~ Star re`？

我需要证明以下命题：

A =~ Star re ->
  B =~ Star re ->
  A ++ B =~ Star re.

该命题是正则表达式泵引理证明的前置引理。

以下是定义正则表达式匹配关系的归纳类型：

Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
  | MEmpty : [] =~ EmptyStr
  | MChar x : [x] =~ (Char x)
  | MApp s1 re1 s2 re2
             (H1 : s1 =~ re1)
             (H2 : s2 =~ re2)
           : (s1 ++ s2) =~ (App re1 re2)
  | MUnionL s1 re1 re2
                (H1 : s1 =~ re1)
              : s1 =~ (Union re1 re2)
  | MUnionR re1 s2 re2
                (H2 : s2 =~ re2)
              : s2 =~ (Union re1 re2)
  | MStar0 re : [] =~ (Star re)
  | MStarApp s1 s2 re
                 (H1 : s1 =~ re)
                 (H2 : s2 =~ (Star re))
               : (s1 ++ s2) =~ (Star re)

  where "s =~ re" := (exp_match s re).

我尝试对假设A =~ Star re使用inversion策略，但递归过程中发现必须调用当前待证的这个命题才能完成证明，不知道该怎么处理，求指导。

内容的提问来源于stack exchange，提问作者Mohammad Teimori Pabandi