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

At: discrete Formula with rank 1 2 1 1 1 2 1
1. x: Formula
2. x1: Formula
3. y@0: Formula
4. x2: Formula
5. x1 = x2

x1 = x2
By:
FormulaEquality -1
THEN
Trivial
Generated subgoals:

None

About:
equal

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