| lapply linear lift_inv_lref_1_le_nplus to H3, H1, H2
| lapply linear lift_inv_bind_1 to H5. decompose
| lapply linear lift_inv_flat_1 to H5. decompose
| lapply linear lift_inv_lref_1_le_nplus to H3, H1, H2
| lapply linear lift_inv_bind_1 to H5. decompose
| lapply linear lift_inv_flat_1 to H5. decompose