At:
equivalence weakening lemma
1
1
1
1.
T: Type
2.
eq: {T=
}
3.
eq 
T
T
4.
x,y:T. eq(x,y) 
x = y
5.
f: {T
}
6.
f TT
7.
x:T. f(x,x)
8.
x,y:T. f(x,y) f(y,x)
9.
x,y,z:T. f(x,y) 
f(y,z) f(x,z)
10.
x: T
11.
y: T
12.
eq(x,y)
13.
x = y
f(x,y)
By:
HypSubst -1 0
THEN
Witness7 y
THEN
Trivial
Generated subgoals:
None
About:
