Nuprl - Pf discrete Var 1

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

At: discrete Var 1

1. x: Atom
2. y: Atom

Dec(x = y)

By: ProveDecidable

Generated subgoals:

None

About:

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