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

At: sublist weakening wrt identity 1 1 1 1
1. T: Type
2. Discrete{T}
3. eq: {T}
4. L: T List
5. M: T List
6. L = M
7. u: T
8. v: T List

u(eq) (u.v)
By: Rewrite (HigherC is_member_unrollC) 0
Generated subgoal:

1 if eq(u,u) true else u(eq) v fi

About:
listconsbtrueifthenelseassertapplyuniverseequal

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