Add some unpleasant machinery for weakening contexts.
Finish the proofs, except now we are postulating that weaking preserves obs equivalence. Fuck.