| 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
- ]; subst; autobatch.
+ ]; destruct; autobatch.
qed.
theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to
lapply lift_inv_lref_2_le_nplus to H3, H0, H2
| lapply linear lift_inv_bind_2 to H5. decompose
| lapply linear lift_inv_flat_2 to H5. decompose
- ]; subst; autobatch.
+ ]; destruct; autobatch.
qed.