E:(T
T
). (x,y:T. E(x,y) 
x = y) 
(i:T, s:(T+T) List. member-left-paren(x,y.E(x,y);i;s) (inl(i) 
s))L:T List, P:(T). (
xL.P(x)) (i:
||L||. P(L[i]))| Rank | Theorem | Name |
| 2 | Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-left-paren(x,y.E(x,y);i;s) (inl(i) s)) | [assert-member-left-paren] |
| cites | ||
| 1 | Thm* L:T List, P:(T). (xL.P(x)) (i:||L||. P(L[i])) | [assert_l_bexists] |