note LCA algorithm in reachability more carefully

[ivoysey]

Reachability is a nice property, but I wonder if it's possible to establish
a more "local" version of reachability.  That one may have to go all the
way up and then down in movements does not bode well for implementation.
For example, if one could characterize paths to a cursor from the top of
the program, then one could prove that the moves necessary do not have to
go higher than the shared prefix of the paths to the two positions.

[ivoysey]

this is actually related to a really cool question i got in my PoP seminar talk about the exact witness you get from constructibility and different algorithms that prove the same theorem. there's maybe something to be said more generally about the witnesses we chose.