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

At: disjoint tail 1
1. T: Type
2. eq: TT
3. L1: T List
4. L2: T List
5. x: T
6. disjoint(eq;(x.L1);L2)

disjoint(eq;L1;L2)
By: Rewrite (HigherC disjoint_unrollC) 6
Generated subgoal:

16. x(eq) L2 & disjoint(eq;L1;L2)
disjoint(eq;L1;L2)

About:
listconsboolfunctionuniverse

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