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

At: discrete Formula 1 2 1 1
1. Q: FormulaProp
2. x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
3. x: Formula
4. Q(x)
5. y@0: Formula
6. x1: Formula

Dec(x = x1)
By: Decide (x = x1)
Generated subgoals:

17. x = x1
Dec(x = x1)
27. x = x1
Dec(x = x1)

About:
decidablesetapplyfunctionequalpropall

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