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

At: sublist reflexive 1 1 1
1. T: Type
2. eq: {T=}
3. eq TT
4. x,y:T. eq(x,y) x = y
5. L: T List
6. u: T
7. v: T List
8. v(eq)v

if eq(u,u) true else u(eq) v fi
By: Assert (eq(u,u))
Generated subgoals:

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

About:
listboolbtrueifthenelseassertapply
functionuniverseequalmemberall

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