(9steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
tail1
1
1
1.
T:
Type
2.
eq:
{T=
}
3.
u:
T
4.
v:
T List
x
v.x(
eq) (u.v)
By:
Rewrite (HigherC is_member_unrollC) 0
Generated subgoal:
1
x
v.if eq(x,u)
true
else x(
eq) v fi
About:
(9steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
x
v.if eq(x,u)
true
else x(eq) v fi}
xv.x(eq) (u.v)
xv.if eq(x,u) true else x(eq) v fi
