English
If LiftRel R holds between two nested streams S and T, then for any a that lies in the membership of S.join.destruct, there exists b in T.join.destruct such that there is a LiftRelO between a and b under R and the lifted relation U.
Русский
Если между двумя вложенными потоками S и T выполняется LiftRel R, то для любого a, принадлежащего к S.join.destruct, существует b в T.join.destruct такой, что существует LiftRelO между a и b под R и вознесенной связью U.
LaTeX
$$$\text{LiftRel } (\text{LiftRel } R)\ S T \rightarrow \forall a \in S.\join.destruct, \exists b \in T.\join.destruct, \; \text{LiftRelO } R U\ a\ b$$$
Lean4
theorem liftRel_bind {δ} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : WSeq α} {s2 : WSeq β} {f1 : α → WSeq γ}
{f2 : β → WSeq δ} (h1 : LiftRel R s1 s2) (h2 : ∀ {a b}, R a b → LiftRel S (f1 a) (f2 b)) :
LiftRel S (bind s1 f1) (bind s2 f2) :=
liftRel_join _ (liftRel_map _ _ h1 @h2)
