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

At: sublist tail 1 1 1 1 1 1 1 1 2
1. T: Type
2. Discrete{T}
3. eq: {T}
4. eq TT
5. u: T
6. v: T List
7. f1: {T=}
8. x,y:T. f1(x,y) eq(x,y)
9. xv.if eq(x,u) true else x(eq) v fi (z:T. z(f1) v if eq(z,u) true else z(eq) v fi)
10. z: T
11. z(f1) v
12. eq(z,u) = false

z(eq) v
By: Using [`eq',f1] (BackThru Thm* eq:{T=}, u:T, L:T List. u(eq) L (f:{T}. u(f) L))
Generated subgoal:

1 z(f1) v

About:
listboolbfalsebtrueifthenelseassertapply
functionuniverseequalmemberimpliesall

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