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

At: discrete Formula 1 5
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)

y@0:Formula. Dec(y2y3 = y@0)
By: Analyze 0
Generated subgoal:

16. y@0: Formula
Dec(y2y3 = y@0)

About:
decidablesetapplyfunctionequalpropall

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