| Rank | Theorem | Name |
| 2 | | | Thm* Discrete{T}   ( eq:{T  }, L,M:T List. (L @ M)( eq)(M @ L)) | [append_commutes_under_sublist] |
| cites |
| 0 | | | Thm* Discrete{T} ( f:{T=}. True) | [discrete_implies_discrete_equality] |
| 1 | | | Thm* eq:{T=}, P:(T  Prop), L:T List. x L.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] |
| 0 | | | Thm* T:Type, EQ:{T=}. EQ {T} | [discrete_equality_is_equivalence] |
| 1 | | | Thm* eq:{T}, L,M:T List, x:T. x(eq) (L @ M) x(eq) (M @ L) | [append_commutes_under_is_member] |