Nuprl - Pf disjoint iff assert disjoint2 1

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

At: disjoint iff assert disjoint2 1

1. T: Type
2. eq: {T}
3. eq TT
4. L: T List
5. M: T List

disjoint(eq;L;M) disjoint(eq;L;M)

By: ListInd 4 THEN Rewrite (HigherC disjoint2_unrollC THENC HigherC disjoint_unrollC) 0

Generated subgoals:

1 True true

2 6. u: T
7. v: T List
8. disjoint(eq;v;M) disjoint(eq;v;M)
u(eq) M & disjoint(eq;v;M) if u(eq) M false else disjoint(eq;v;M) fi

About:

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