At:
discrete equality unique
1
1
1
1
1
1
1
1
1
1
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) = true
9.
f2(v,w) = false
10.
True 
(v = w)
11.
False 
v = w
12.
False (v = w)
13.
v = w
true = false
By:
FwdThru -2 [-1]
Generated subgoals:
None
About:
