equiv:{T
}, eq:{T=}, u:T, L:T List. u(
equiv) L 
(
v:T. equiv(u,v) & v(eq) L)eq:{T}, L:T List, x:T. x(eq) L (M,N:T List, y:T. eq(x,y) & L = (M @ (y.N)))eq:{T=}, L:T List, x:T. (M,N:T List. L = (M @ (x.N))) x(eq) L| Rank | Theorem | Name | ||
| 2 | Thm* equiv:{T}, eq:{T=}, u:T, L:T List. u(equiv) L (v:T. equiv(u,v) & v(eq) L) | [is_member_equality_strengthening_lemma] | ||
| cites | ||||
| 1 | Thm* eq:{T}, L:T List, x:T. x(eq) L (M,N:T List, y:T. eq(x,y) & L = (M @ (y.N))) | [is_member_append_lemma1] | ||
| 0 | Thm* eq:{T=}, L:T List, x:T. (M,N:T List. L = (M @ (x.N))) x(eq) L | [append_is_member_lemma] |