English
A distributive law holds for nested dite and ite on the right: dite p (fun hp => dite q (a hp) (b hp)) c equals dite q (fun hq => dite p (fun hp => a hp hq) c) (fun hq => dite p (fun hp => b hp hq) c).
Русский
Существует правая дистрибутивность вложенного dite и ite: dite p (...) = dite q (...) ...
LaTeX
$$$ \operatorname{dite}(p)(\lambda hp.\operatorname{dite}(q)(a(hp))(b(hp)))(c) = \operatorname{dite}(q)(\lambda hq. \operatorname{dite}(p)(\lambda hp. a(hp)(hq)) \, c) (\operatorname{dite}(p)(\lambda hp. b(hp)(hq)) \, c) $$$
Lean4
theorem dite_dite_distrib_right {a : p → q → α} {b : p → ¬q → α} {c : ¬p → α} :
dite p (fun hp ↦ dite q (a hp) (b hp)) c =
dite q (fun hq ↦ dite p (fun hp ↦ a hp hq) c) fun hq ↦ dite p (fun hp ↦ b hp hq) c :=
by split_ifs <;> rfl
