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

At: discrete Formula with rank 1
1. x: Formula

y:Formula. Dec(x = y)
By: FormulaRankInd -1
Generated subgoals:

12. x2: Var
y:Formula. Dec(x2 = y)
22. x1: Formula
3. y:Formula. Dec(x1 = y)
y@0:Formula. Dec(x1 = y@0)
32. x2: Formula
3. x3: Formula
4. y:Formula. Dec(x2 = y)
5. y:Formula. Dec(x3 = y)
y@0:Formula. Dec(x2x3 = y@0)
42. x2: Formula
3. x3: Formula
4. y:Formula. Dec(x2 = y)
5. y:Formula. Dec(x3 = y)
y@0:Formula. Dec(x2x3 = y@0)
52. y1: Formula
3. y2: Formula
4. y:Formula. Dec(y1 = y)
5. y:Formula. Dec(y2 = y)
y@0:Formula. Dec(y1y2 = y@0)

About:
decidableequalall

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