broken but promising
here wo show that reachable_spoofing is useless
theorem reachable_eq_rtrancl_view
cleanup
refactored
comments, finite, and tuned notation
tuned notation