At:
is member tail1
1.
T: Type
2.
eq: {T}
3.
eq TT
4.
x:T. eq(x,x)
5.
x,y:T. eq(x,y) eq(y,x)
6.
x,y,z:T. eq(x,y) eq(y,z) eq(x,z)
7.
x: T
8.
L: T List
9.
x(eq) L
10.
y: T
x(eq) (y.L)
By:
Rewrite (HigherC is_member_unrollC) 0
THEN
GenConcl (eq(x,y) = b)
THEN
BoolInd -2
THEN
Rewrite (HigherC ifthenelse_evalC THENC TryC (HigherC assert_evalC)) 0
THEN
Trivial
Generated subgoals:
}
T
T
x:T. eq(x,x)
eq(y,x)
x(