Add oav2 and oasuc to iset.mm
Add oav2 and oasuc to iset.mm

oav2 is an expression for the value of addition. Maybe just
interesting as an oasuc lemma, but might be more broadly
interesting (we'll see).

oasuc is stated as in set.mm and the proof is the one outlined
by Mario Carneiro on github.

metamath/set.mm,metamath/set.mm,metamath/set.mm