At:
discrete equality unique
1
1
1
1
1
1
1
1
1
2
1
1.
T: Type
2.
f1: T
T
3.
f1 
TT
4.
f2: TT
5.
f2 TT
6.
v: T
7.
w: T
8.
f1(v,w) = false
9.
f2(v,w) = true
10.
False 
v = w
11.
False 
(v = w)
12.
True (v = w)
13.
v = w
false = true
By:
FwdThru -3 [-1]
Generated subgoals:
None
About:
