Nuprl - Pf disjoint iff assert disjoint2 1 2 2

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

At: disjoint iff assert disjoint2 1 2 2

1. T: Type
2. eq: {T}
3. eq TT
4. L: T List
5. M: T List
6. u: T
7. v: T List
8. disjoint(eq;v;M) disjoint(eq;v;M)
9. u(eq) M = false

true & disjoint(eq;v;M) disjoint(eq;v;M)

By: Rewrite (HigherC assert_evalC) 0

Generated subgoals:

1 8. disjoint(eq;v;M) disjoint(eq;v;M)
9. disjoint(eq;v;M) disjoint(eq;v;M)
10. u(eq) M = false
11. True
12. disjoint(eq;v;M)
disjoint(eq;v;M)

2 8. disjoint(eq;v;M) disjoint(eq;v;M)
9. disjoint(eq;v;M) disjoint(eq;v;M)
10. u(eq) M = false
11. disjoint(eq;v;M)
disjoint(eq;v;M)

About:

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