re_not_empty.v

Fixpoint re_not_empty {T : Type} (re : reg_exp T) : bool :=
  match re with
  | EmptySet => false
  | EmptyStr => true
  | Char _ => true
  | App re1 re2 => andb (re_not_empty re1) (re_not_empty re2)
  | Union re1 re2 => orb (re_not_empty re1) (re_not_empty re2)
  | Star re => true (* always match empty string *)
  end.

Lemma re_not_empty_correct : forall T (re : reg_exp T),
  (exists s, s =~ re) <-> re_not_empty re = true.
Proof.
  split; intros. generalize dependent re.
  induction re. intros H. destruct H. inversion H.
  intros H. destruct H. simpl. auto.
  intros H. simpl. auto.
  intros H. simpl. apply andb_true_iff. destruct H.
  split. apply IHre1. inversion H. exists s1. assumption.
  apply IHre2. inversion H. exists s2. assumption.
  intros H. simpl. apply orb_true_iff. destruct H.
  inversion H. left. apply IHre1. exists x. assumption.
  right. apply IHre2. exists x. assumption.
  intros H. auto.

  T : Type
  re : reg_exp T
  H : re_not_empty re = true
  ============================
  exists s : list T, s =~ re

I am wondering re_not_empty should be (Any counter example ?)

Fixpoint re_not_empty {T : Type} (re : reg_exp T) : bool :=
match re with
| EmptySet => false
| _ => true
end.