- [ intros. clear H1.
- lapply linear track_inv_lref to H. decompose.
- lapply insert_inv_leaf_2 to H. decompose
- | intros.
- lapply linear track_inv_parx to H. subst. autobatch.
- | intros.
- lapply linear track_inv_impw to H1.
- decompose. subst.
- lapply linear H to H4, H2. decompose. autobatch
- | intros 3. elim q; clear q;
- [ clear H H1.
- lapply linear track_inv_lref to H2. decompose.
- lapply insert_inv_leaf_2 to H. decompose
- | lapply linear track_inv_parx to H2. subst. autobatch
- | clear H H1.
- lapply linear track_inv_impi to H2.
- lapply linear track_inv_impw to H3.
- decompose. subst. autobatch
- | clear H H1 H2.
- lapply linear track_inv_impi to H3.
- decompose. subst
- | clear H H1.
- lapply linear track_inv_impi to H2.
- lapply linear track_inv_impe to H3.
- decompose. subst. autobatch
+ [ intros; clear H1;
+ lapply linear track_inv_lref to H; decompose;
+ lapply insert_inv_leaf_2 to H; decompose
+ | intros;
+ lapply linear track_inv_parx to H; subst; autobatch;
+ | intros;
+ lapply linear track_inv_impw to H1;
+ decompose; subst;
+ lapply linear H to H4, H2; decompose; autobatch
+ | intros 3; elim q; clear q;
+ [ clear H H1;
+ lapply linear track_inv_lref to H2; decompose;
+ lapply insert_inv_leaf_2 to H; decompose
+ | lapply linear track_inv_parx to H2; subst; autobatch
+ | clear H H1;
+ lapply linear track_inv_impr to H2;
+ lapply linear track_inv_impw to H3;
+ decompose; subst; autobatch
+ | clear H H1 H2;
+ lapply linear track_inv_impr to H3;
+ decompose; subst
+ | clear H2 H3;
+ lapply linear track_inv_impr to H4;
+ lapply linear track_inv_impi to H5;
+ decompose; subst;
+ lapply linear H to H5, H8; decompose;
+
+
+ lapply linear insert_inv_leaf_1 to H4; decompose; subst;
+ apply ex_intro; [| ]
+
+ autobatch depth = 100 width = 40 size = 100