theorem obindeq1 (_a1 _a2: nat) (F: set): $ _a1 = _a2 -> obind _a1 F = obind _a2 F $;
_a1 = _a2 -> _a1 = _a2
_a1 = _a2 -> obind _a1 F = obind _a2 F