(
eq:{T
}, u:T, v:T List. v(
eq)(u.v)) (
f:{T=}. True)eq:{T=}, f:{T}, x,y:T. eq(x,y) f(x,y)eq:{T=}, P:(T
Prop), L:T List. x
L.P(x) 
(z:T. z(eq) L P(z))eq:{T=}, u:T, L:T List. u(eq) L (f:{T}. u(f) L)| Rank | Theorem | Name | ||
| 2 | Thm* Discrete{T} (eq:{T}, u:T, v:T List. v(eq)(u.v)) | [sublist_tail] | ||
| cites | ||||
| 0 | Thm* Discrete{T} (f:{T=}. True) | [discrete_implies_discrete_equality] | ||
| 0 | Thm* eq:{T=}, f:{T}, x,y:T. eq(x,y) f(x,y) | [equivalence_weakening_lemma] | ||
| 1 | Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) | [list_all_is_member_lemma] | ||
| 1 | Thm* eq:{T=}, u:T, L:T List. u(eq) L (f:{T}. u(f) L) | [is_member_equalities_lemma] |