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

At: discrete Formula with rank 1 1 1 1 1
1. x: Formula
2. x2: Var
3. y: Formula
4. x3: Var
5. x2 = x3

Dec(x2 = x3)
By:
TrueCase
THEN
FormulaEquality 0
THEN
Trivial
Generated subgoals:

None

About:
decidableequal

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