T:Type{i}, x:T, L:T List, P:(T
TProp{i'}).
Thm* (
x,y
[x / L].P(x,y)) 
(x,yL.P(x,y)) & (yL.P(x,y))L:T List, i:
||L||. (L[i] L)x:T, l:T List, i:||l||. [x / l][(i+1)] ~ l[i]| Theorem | Name |
| T:Type{i}, x:T, L:T List, P:(TTProp{i'}).
Thm* ( x,y[x / L].P(x,y)) (x,yL.P(x,y)) & (yL.P(x,y)) | [pairwise-cons] |
| cites the following: | |
| L:T List, i:||L||. (L[i] L) | [select_member] |
| x:T, l:T List, i:||l||. [x / l][(i+1)] ~ l[i] | [select_cons_tl_sq] |