Optlang: Get base cases working in opt valid
Optlang: Rearrange proof to make dealing with pairs easier
Optlang: Remove unneeded conversions