Nuprl - Pf is member of append lemma 1 2 2 1

(16steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

1. T: Type
2. eq: {T}
3. L: T List
4. M: T List
5. x: T
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

if eq(x,u) true else x(eq) (v @ M) fi

By: IfThenElseCases 0 THEN Reduce 0

Generated subgoals:

1 10. eq(x,u) = true
True

2 10. eq(x,u) = false
x(eq) (v @ M)

About:

(16steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

1	10. `eq(x,u) = true` `True`
2	10. `eq(x,u) = false` `x(eq) (v @ M)`