English
If s and t are related by LiftRel R, then for every n, the destruct of drop s n is related to the destruct of drop t n by LiftRelO R (LiftRel R).
Русский
Если s и t связаны relation LiftRel R, то для каждого n их drop s n и drop t n после destruct связаныLiftRelO R (LiftRel R).
LaTeX
$$$\forall R\,\forall s,t\left(H: \mathrm{LiftRel}\ R\ s\ t\right),\ \forall n:\mathbb{N},\ \mathrm{LiftRel}(\mathrm{LiftRelO}(R,\mathrm{LiftRel}(R)))(\mathrm{destruct}(\mathrm{drop}(s,n)))(\mathrm{destruct}(\mathrm{drop}(t,n)))$$$
Lean4
theorem liftRel_dropn_destruct {R : α → β → Prop} {s t} (H : LiftRel R s t) :
∀ n, Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct (drop s n)) (destruct (drop t n))
| 0 => liftRel_destruct H
| n + 1 => by
simp only [drop, destruct_tail]
apply liftRel_bind
· apply liftRel_dropn_destruct H n
exact fun {a b} o =>
match a, b, o with
| none, none, _ => by simp
| some (a, s), some (b, t), ⟨_, h2⟩ => by simpa [tail.aux] using liftRel_destruct h2
