(2steps) PrintForm Definitions Lemmas formula equality Sections ClassicalProps(jlc) Doc

At: decidable equal Formula

F,F':Formula. Dec(F = F')
By:
Inst Thm* Discrete{Formula} []
THEN
UnfoldTopAb -1
Generated subgoal:

11. x,y:Formula. Dec(x = y)
F,F':Formula. Dec(F = F')

About:
decidableequalall

(2steps) PrintForm Definitions Lemmas formula equality Sections ClassicalProps(jlc) Doc