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

At: discrete Formula 1 3 1 1 1 1
1. Q: FormulaProp
2. x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
3. x1: {x:Formula| Q(x) }
4. x2: Formula
5. Q(x2)
6. y@0: Formula
7. x3: Formula
8. x4: Formula
9. x1 = x3
10. x2 = x4

Dec(x1x2 = x3x4)
By:
TrueCase
THEN
FormulaEquality 0
Generated subgoals:

None

About:
decidablesetapplyfunctionequalpropall

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