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