still_no_idea.v

Lemma MStar'' : forall T (s : list T) (re : reg_exp T),
    s =~ Star re ->
    exists ss : list (list T),
      s = fold app ss []
      /\ forall s', In s' ss -> s' =~ re.
Proof.
  intros T s re H. remember (Star re) as re'. induction H.
  inversion Heqre'.
  inversion Heqre'.
  inversion Heqre'.
  inversion Heqre'.
  inversion Heqre'.
  inversion Heqre'. exists []. simpl. intuition.
  inversion Heqre'; subst re0.
  specialize (IHexp_match2 Heqre'). destruct IHexp_match2 as [ss2 IHx]. 
  destruct IHx. 
  
   T : Type
  re : reg_exp T
  s1, s2 : list T
  Heqre' : Star re = Star re
  H : s1 =~ re
  H0 : s2 =~ Star re
  IHexp_match1 : re = Star re ->
                 exists ss : list (list T),
                   s1 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)
  ss2 : list (list T)
  H1 : s2 = fold app ss2 [ ]
  H2 : forall s' : list T, In s' ss2 -> s' =~ re
  ============================
  exists ss : list (list T),
    s1 ++ s2 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)