(2steps) PrintForm Definitions var jlc Sections ClassicalProps(jlc) Doc

At: discrete Var

Discrete{Var}
By:
Unfolds [`discrete`;`Var`] 0
THEN
UnivCD
Generated subgoal:

11. x: Atom
2. y: Atom
Dec(x = y)

About:
decidableatomequal

(2steps) PrintForm Definitions var jlc Sections ClassicalProps(jlc) Doc