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

At: discrete Formula with rank 1 5
1. x: Formula
2. y1: Formula
3. y2: Formula
4. y:Formula. Dec(y1 = y)
5. y:Formula. Dec(y2 = y)

y@0:Formula. Dec(y1y2 = y@0)
By: Analyze 0
Generated subgoal:

16. y@0: Formula
Dec(y1y2 = y@0)

About:
decidableequalall

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