(4steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
At:
equivalence
weakening
lemma
1
1.
T:
Type
2.
eq:
{T=
}
3.
f:
{T
}
4.
x:
T
5.
y:
T
eq(x,y)
f(x,y)
By:
DiscreteEq 2
THEN
Analyze 0
Generated subgoal:
1
3.
eq
T
T
4.
x,y:T. eq(x,y)
x = y
5.
f:
{T
}
6.
x:
T
7.
y:
T
8.
eq(x,y)
f(x,y)
About:
(4steps)
PrintForm
Definitions
core
3
jlc
Sections
Support(jlc)
Doc
T
T
x,y:T. eq(x,y) 
x = y
}
f(x,y)}
}
eq(x,y) 
f(x,y)
TTx,y:T. eq(x,y) x = y} f(x,y)
