theorem lift_total: \forall l, t, i. \exists u. Lift l i t u.
intros 2. elim t; clear t;
- [ auto
+ [ autobatch
| lapply (nle_gt_or_le n i). decompose;
- [ auto
- | lapply (nplus_total l n). decompose. auto
+ [ autobatch
+ | lapply (nplus_total l n). decompose. autobatch
]
- | lapply (H i1). lapply (H1 (succ i1)). decompose. auto
- | lapply (H i1). lapply (H1 i1). decompose. auto
+ | lapply (H i1). lapply (H1 (succ i1)). decompose. autobatch
+ | lapply (H i1). lapply (H1 i1). decompose. autobatch
].
qed.
| 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; auto.
+ ]; 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; auto.
+ ]; destruct; autobatch.
qed.