(42steps) PrintForm Definitions formula equality Sections ClassicalProps(jlc) Doc

At: discrete Formula

Discrete{Formula}
By:
UnfoldTopAb 0
THEN
Analyze 0
Generated subgoal:

11. x: Formula
y:Formula. Dec(x = y)

About:
decidableequalall

(42steps) PrintForm Definitions formula equality Sections ClassicalProps(jlc) Doc