(
eq1,eq2,eq3:{T
}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(
eq1)L2 L2(eq2)L3 L1(eq3)L3) (
f:{T=}. True)eq:{T=}, P:(T
Prop), L:T List. x
L.P(x) 
(z:T. z(eq) L P(z))P:
. P P = true| Rank | Theorem | Name | ||
| 2 | Thm* Discrete{T} (eq1,eq2,eq3:{T}, L1,L2,L3:T List. eq1 = eq2 eq2 = eq3 L1(eq1)L2 L2(eq2)L3 L1(eq3)L3) | [sublist_transitivity] | ||
| cites | ||||
| 0 | Thm* Discrete{T} (f:{T=}. True) | [discrete_implies_discrete_equality] | ||
| 1 | Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) | [list_all_is_member_lemma] | ||
| 0 | Thm* P:. P P = true | [assert_iff_btrue] |