- Lift l i (leaf (lref j1)) x \to
- i <= j1 \to \forall j2. (l + j1 == j2) \to
- x = leaf (lref j2).
- intros 5.
- lapply linear lift_inv_lref_1 to H. decompose; subst;
+ Lift l i (lref j1) x \to i <= j1 \to
+ \exists j2. (l + j1 == j2) \land x = lref j2.
+ intros.
+ lapply linear lift_inv_lref_1 to H. decompose; destruct;
+ [ lapply linear nle_false to H1, H2. decompose
+ | autobatch
+ ].
+qed.
+
+theorem lift_inv_lref_1_le_nplus: \forall l, i, j1, x.
+ Lift l i (lref j1) x \to
+ i <= j1 \to \forall j2. (l + j1 == j2) \to
+ x = lref j2.
+ intros.
+ lapply linear lift_inv_lref_1 to H. decompose; destruct;