Theorem: Metamath.DJ.ne (Metamath/Translate.lean)

State before:
dj : DJ
a b : VR
h : disj dj a b
e : a = b
⊢ False
Tactic:
cases e
State after:
case refl
dj : DJ
a : VR
h : disj dj a a
⊢ False

State before:
case refl
dj : DJ
a : VR
h : disj dj a a
⊢ False
Tactic:
exact dj.irr h
State after:
no goals