3 ms·

How do you make contraction happen? I don't see a button for it.

• ezyang 14y ago
  We do contraction on implication-left automatically, and only have it as an option for forall-left and exists-right, since it's not a useful notion for the other operators.