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

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

Dec(x1 = x)
By:
FalseCase
THEN
Analyze -2
Generated subgoal:

16. x1 = x
x1 = x

About:
decidablesetapplyfunctionequalpropall

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