English
If R is strengthened to S and C to D, then LiftRelO R C implies LiftRelO S D.
Русский
Если R усиливается до S, а C до D, то возводя LiftRelO, имеем: LiftRelO R C ⇒ LiftRelO S D.
LaTeX
$$$$ (\forall a,b,\ R\ a\ b \to S\ a\ b) \land (\forall s,t,\ C\ s\ t \to D\ s\ t) \Rightarrow \forall o p,\ \mathrm{LiftRelO}\ R\ C\ o\ p\Rightarrow \mathrm{LiftRelO}\ S\ D\ o\ p. $$$$
Lean4
theorem imp {R S : α → β → Prop} {C D : WSeq α → WSeq β → Prop} (H1 : ∀ a b, R a b → S a b)
(H2 : ∀ s t, C s t → D s t) : ∀ {o p}, LiftRelO R C o p → LiftRelO S D o p
| none, none, _ => trivial
| some (_, _), some (_, _), h => And.imp (H1 _ _) (H2 _ _) h
| none, some _, h => False.elim h
| some (_, _), none, h => False.elim h
