At:
is member append disjunction lemma122121
1.
T: Type
2.
eq: {T}
3.
x: T
4.
L: T List
5.
M: T List
6.
u: T
7.
v: T List
8.
x(eq) v x(eq) M x(eq) (v @ M)
9.
if eq(x,u) true else x(eq) v fi x(eq) M
10.
eq(x,u) = false
x(eq) v x(eq) M
By:
HypSubst -1 -2
THEN
Reduce -2
Generated subgoal:
1
9. x(eq) v x(eq) M 10. eq(x,u) = false x(eq) v x(eq) M
eq) v 
x(
x(
x(
true
