-
David Swasey authored
Simplified adv, defining it with ownL. Proof of concept for a friendly interface that (if it works) lets the user set up an invariant and prove view shifts and atomic triples for primitive reductions, rather than work in the model. (It should work, but I have to merge my two proofs to make sure.)
1fe7ecef