Is there a tactic to help resolving existential quantifiers in Coq?
I was similarly stuck on this problem. I believe your Fixpoint for Star re should just be true. In regular expressions, the empty string is always accepted under star.