At:
sublist reflexive11121
1.
T: Type
2.
eq: {T=}
3.
eq TT
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)
10.
eq(u,u) = true
if eq(u,u) true else u(eq) v fi
By:
HypSubst -1 0
THEN
Reduce 0
THEN
Trivial
Generated subgoals:
}
T
T
x,y:T. eq(x,y) 
x = y
eq)v
if eq(u,u)
true
