theorem lift_inv_sort_1: \forall l, i, h, x.
Lift l i (sort h) x \to
x = sort h.
theorem lift_inv_sort_1: \forall l, i, h, x.
Lift l i (sort h) x \to
x = sort h.
qed.
theorem lift_inv_lref_1: \forall l, i, j1, x.
qed.
theorem lift_inv_lref_1: \forall l, i, j1, x.
- intros. inversion H; clear H; intros;
- [ destruct H1
- | destruct H2. clear H2. subst. auto
- | destruct H3. clear H3. subst. auto depth = 5
- | destruct H5
- | destruct H5
- ].
+ intros. inversion H; clear H; intros; destruct; autobatch depth = 5 size = 7.
qed.
theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
qed.
theorem lift_inv_bind_1: \forall l, i, r, u1, t1, x.
qed.
theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
qed.
theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
qed.
theorem lift_inv_sort_2: \forall l, i, x, h.
Lift l i x (sort h) \to
x = sort h.
qed.
theorem lift_inv_sort_2: \forall l, i, x, h.
Lift l i x (sort h) \to
x = sort h.
qed.
theorem lift_inv_lref_2: \forall l, i, x, j2.
qed.
theorem lift_inv_lref_2: \forall l, i, x, j2.
- intros. inversion H; clear H; intros;
- [ destruct H2
- | destruct H3. clear H3. subst. auto
- | destruct H4. clear H4. subst. auto depth = 5
- | destruct H6
- | destruct H6
- ].
+ intros. inversion H; clear H; intros; destruct; autobatch depth = 5 size = 10.
qed.
theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
qed.
theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
qed.
theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
qed.
theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
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.
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.