f:(
D:Type. D
(D List)), A:Type, a:A, B:Type, b:B.
Thm* ||f(a)|| = ||f(b)||
f:(D:Type. DT), A:Type, a:A, B:Type, b:B. f(a) = f(b) T| Theorem | Name |
| f:(D:Type. D(D List)), A:Type, a:A, B:Type, b:B.
Thm* ||f(a)|| = ||f(b)|| | [sfa_doc_type_poly_len_const] |
| cites the following: | |
| f:(D:Type. DT), A:Type, a:A, B:Type, b:B. f(a) = f(b) T | [sfa_doc_type_poly_constant] |