coq - IndProp: re_not_empty_correct

Question

Lemma re_not_empty_correct : forall T (re : @reg_exp T),
  (exists s, s =~ re) <-> re_not_empty re = true.
Proof.
  split.
  - admit. (* I proved it myself *)
  - intros. induction re.
    + simpl in H. discriminate H.
    + exists []. apply MEmpty.
    + exists [t]. apply MChar.
    + simpl in H. rewrite -> andb_true_iff in H. destruct H as [H1 H2].
      apply IHre1 in H1. apply IHre2 in H2.

これまでに得たものは次のとおりです。

1 subgoal (ID 505)

T : Type
re1, re2 : reg_exp
H1 : exists s : list T, s =~ re1
H2 : exists s : list T, s =~ re2
IHre1 : re_not_empty re1 = true -> exists s : list T, s =~ re1
IHre2 : re_not_empty re2 = true -> exists s : list T, s =~ re2
============================
exists s : list T, s =~ App re1 re2

ここで、H1 と H2 を結合するかexists s : list T, s =~ App re1 re2、ゴールを 2 つのサブゴールに分解し、H1 と H2 を使用してそれらを別々に証明する必要があります。しかし、私はそれを行う方法がわからない。