Flèche-based "almost physical" state eq

Full goal equality; much faster than calling goals as it won't unelaborate them. Note that this may not fully capture proof state equality (it is possible to have similar goals but different evar_maps, but should be enough for all practical users.