(8steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
reflexive
1
1
1
2
1.
T:
Type
2.
eq:
{T=
}
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
9.
eq(u,u)
if eq(u,u)
true
else u(
eq) v fi
By:
FwdThru
Thm*
P:
. P
P = true
[-1]
Generated subgoal:
1
10.
eq(u,u) = true
if eq(u,u)
true
else u(
eq) v fi
About:
(8steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
if eq(u,u)
true else u(
eq) v fi}
T
T
x,y:T. eq(x,y) 
x = y
eq)v
if eq(u,u) true else u(eq) v fi
P:. P P = true
[-1]
if eq(u,u) true else u(eq) v fi
