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.


T : Type
  re, re0 : reg_exp T
  Heqre' : Star re0 = Star re
  s1, s2 : list T
  H : s1 =~ re0
  H0 : s2 =~ Star re0
  IHexp_match1 : re0 = Star re ->
                 exists ss : list (list T),
                   s1 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)
  IHexp_match2 : Star re0 = Star re ->
                 exists ss : list (list T),
                   s2 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)
  ============================
  exists ss : list (list T),
    s1 ++ s2 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)