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.
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.
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
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