English
If f2 a2 = f2 b2, then FRespects f2 tr a2 b1 is equivalent to FRespects f2 tr b2 b1 for all b1.
Русский
Если f2 a2 = f2 b2, то FRespects f2 tr a2 b1 эквивалентно FRespects f2 tr b2 b1 для всех b1.
LaTeX
$$$\\forall {\\sigma_1 \\sigma_2} {f_2 : \\sigma_2 \\to \\mathrm{Option}\\,\\sigma_2} {tr : \\sigma_1 \\to \\sigma_2} {a_2 b_2}, f_2\\ a_2 = f_2\\ b_2 \\Rightarrow \\forall {b_1},\\ FRespects f_2 tr a_2 b_1 \\Leftrightarrow FRespects f_2 tr b_2 b_1$$$
Lean4
theorem frespects_eq {σ₁ σ₂} {f₂ : σ₂ → Option σ₂} {tr : σ₁ → σ₂} {a₂ b₂} (h : f₂ a₂ = f₂ b₂) :
∀ {b₁}, FRespects f₂ tr a₂ b₁ ↔ FRespects f₂ tr b₂ b₁
| some _ => reaches₁_eq h
| none => by unfold FRespects; rw [h]