k:
, L1,L2:(k-1) List.
Thm* compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2)
f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as'))| Theorem | Name |
| k:, L1,L2:(k-1) List.
Thm* compose_flips(L1) o compose_flips(L2) = compose_flips(L1 @ L2) | [compose_flips_append] |
| cites the following: | |
| f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as')) | [map_append_sq] |