As discussed with @robbertkrebbers. I proved most of the lemmas corresponding to map_Forall.
map_Forall