Nuprl - Pf discrete Formula 1 5 1 1 1 2

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

1. Q: FormulaProp
2. x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
3. y2: {x:Formula| Q(x) }
4. y3: Formula
5. Q(y3)
6. y@0: Formula
7. y1: Formula
8. y4: Formula
9. y2 = y1
10. y3 = y4

Dec(y2y3 = y1y4)

By: FalseCase THEN Analyze -2 THEN FormulaEquality -1 THEN Trivial

Generated subgoals:

None

About:

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