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

At: decidable disjoint

T:Type, eq:(TT), L1,L2:T List. Dec(disjoint(eq;L1;L2))
By: UnivCD
Generated subgoal:

11. T: Type
2. eq: TT
3. L1: T List
4. L2: T List
Dec(disjoint(eq;L1;L2))

About:
listbooldecidablefunctionuniverseall

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