-theorem lift_conf: \forall l,i,t,x. Lift l i t x \to
- \forall y. Lift l i t y \to
- x = y.
- intros 5. elim H; clear H i t x;
- [ lapply linear lift_inv_sort_1 to H1.
- subst. auto
- | lapply linear lift_inv_lref_1 to H2.
- decompose; subst;
- [ auto | lapply nle_false to H2, H1. decompose ]
- | lapply linear lift_inv_lref_1 to H3.
- decompose; subst;
- [ lapply linear nle_false to H1, H3. decompose
- | lapply linear nplus_conf to H2, H4. subst. auto
- ]
- | lapply linear lift_inv_bind_1 to H5.
- decompose. subst. auto.
- | lapply linear lift_inv_flat_1 to H5.
- decompose. subst. auto.
+(* NOTE: this holds because of nplus_comm_1 *)
+theorem lift_comp: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
+ \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
+ \forall x. Lift l2 i2 t2 x \to
+ \forall i,y. Lift l1 i u1 y \to
+ i1 >= i2 \to (l2 + i1 == i) \to x = y.
+ intros 5. elim H; clear H i1 t1 t2;
+ [ lapply lift_mono to H1, H2. clear H2. destruct.
+ lapply linear lift_inv_sort_1 to H1. destruct.
+ lapply linear lift_inv_sort_1 to H3. destruct. autobatch
+ | lapply lift_mono to H2, H3. clear H3. destruct.
+ lapply linear lift_inv_lref_1 to H2.
+ decompose; destruct; clear H2 H5;
+ lapply linear lift_inv_lref_1_gt to H4; destruct; autobatch width = 4
+ | lapply lift_inv_lref_1_le to H3; [ 2: autobatch ]. clear H3.
+ lapply lift_inv_lref_1_le to H4; [ 2: autobatch ]. clear H4.
+ decompose. destruct. clear H6 i2.
+ lapply lift_inv_lref_1_le to H5; [ 2: autobatch depth = 4 width = 4 ].
+ decompose. destruct. clear H5 H1 H7 i. autobatch depth = 4 size = 7
+ | clear H1 H3.
+ lapply linear lift_inv_bind_1 to H5.
+ lapply linear lift_inv_bind_1 to H6. decompose. destruct.
+ lapply linear lift_inv_bind_1 to H7. decompose. destruct.
+ autobatch depth = 4 width = 6 size = 15
+ | clear H1 H3.
+ lapply linear lift_inv_flat_1 to H5.
+ lapply linear lift_inv_flat_1 to H6. decompose. destruct.
+ lapply linear lift_inv_flat_1 to H7. decompose. destruct.
+ autobatch depth = 4 width = 6 size = 9