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

At: discrete Formula 1 1
1. Q: FormulaProp
2. x:{x:Formula| Q(x) }, y:Formula. Dec(x = y)
3. x1: Var

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

14. y: Formula
Dec(x1 = y)

About:
decidablesetapplyfunctionequalpropall

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