Nuprl - Pf disjoint2 wf 1 1

At: disjoint2 wf 1 1

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

disjoint(eq;L;M)

By: ListInd 4 THEN Rewrite (HigherC disjoint2_unrollC) 0

Generated subgoals:

1 true

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

About:

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