(8steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
reflexive
1
1
1.
T:
Type
2.
eq:
{T=
}
3.
L:
T List
4.
u:
T
5.
v:
T List
6.
v(
eq)v
if eq(u,u)
true
else u(
eq) v fi
By:
DiscreteEq 2
Generated subgoal:
1
3.
eq
T
T
4.
x,y:T. eq(x,y)
x = y
5.
L:
T List
6.
u:
T
7.
v:
T List
8.
v(
eq)v
if eq(u,u)
true
else u(
eq) v fi
About:
(8steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc