P.109 Last case of r_match #11
Description
I think It should be
r_match_star2 : ∀ s s’ r0,
r_match s r0 → r_match s’ (r_star r0) → r_match (s ++ s’) (r_star r0){{ message }}
P.109 Last case of
r_match #11I think It should be
r_match_star2 : ∀ s s’ r0,
r_match s r0 → r_match s’ (r_star r0) → r_match (s ++ s’) (r_star r0)