Nuprl - Pf is member cons 1 2

(6steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc

At: is member cons 1 2

1. T: Type
2. eq: {T}
3. t: T
4. L: T List
5. eq(t,t) = false

t(eq) L

By: FwdThru Thm* P:. P P = false [-1] THEN Analyze -1

Generated subgoal:

1 eq(t,t)

About:

(6steps) PrintForm Definitions Lemmas list 3 jlc Sections Support(jlc) Doc