Intuitionize binom2 in iset.mm
Intuitionize binom2 in iset.mm

Replace the deduction theorem with a proof based on the binom2i one,
but in deduction form.

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