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

At: sublist tail 1
1. T: Type
2. Discrete{T}
3. eq: {T}
4. u: T
5. v: T List

v(eq)(u.v)
By: Rewrite (UnfoldC `sublist` THENC HigherC is_member_unrollC) 0
Generated subgoal:

1 xv.if eq(x,u) true else x(eq) v fi

About:
listconsbtrueifthenelseassertapplyuniverse

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