Inline ovec in addsrpr proof in set.mm
Inline ovec in addsrpr proof in set.mm

Rough idea here is that ovec only has two usages and we can get
wins in file size and clarity by removing it.

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