Indprop.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'. remember s as s'. induction H.
  exists []. simpl. intuition.
  inversion Heqre'.
  inversion Heqre'.
  inversion Heqre'.
  inversion Heqre'.
  inversion Heqre'. exists []. simpl. intuition.
  exists ([s1] ++ [s2]). split. simpl. rewrite app_nil_r. reflexivity.
  intros s' Hin. rewrite in_app_iff in *. destruct Hin.
  
 T : Type
  s : list T
  re, re0 : reg_exp T
  Heqre' : Star re0 = Star re
  s1, s2 : list T
  Heqs' : s1 ++ s2 = s
  H : s1 =~ re0
  H0 : s2 =~ Star re0
  IHexp_match1 : re0 = Star re ->
                 s1 = s ->
                 exists ss : list (list T),
                   s1 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)
  IHexp_match2 : Star re0 = Star re ->
                 s2 = s ->
                 exists ss : list (list T),
                   s2 = fold app ss [ ] /\ (forall s' : list T, In s' ss -> s' =~ re)
  s' : list T
  H1 : In s' [s1]
  ============================
  s' =~ re

subgoal 2 (ID 637) is:
 s' =~ re