feat(data/quot): add map', hrec_on', and hrec_on₂' (#3148) Also add a few simp lemmas
map'
hrec_on'
hrec_on₂'
simp