neqcom
Theorem.
Arguments:
(obj),
(obj),
Assertions:
((
)
(
))
Proof:
Hyp
Ref
Line
Expr
com
1
((
)
(
))
1
eqneqi
2
((
)
(
))