English
There is a distributive law for nested conditional expressions: the expression dite p a (dite q (b p) (c p)) equals the nested dite expression with q and p interchanged in the appropriate branches.
Русский
Существуют правила дистрибутивности вложенных конструкций с dite: левая лестничная композиция превращается в эквивалентную формуцу.
LaTeX
$$$ \operatorname{dite}(p)(a)\bigl(\lambda hp.\operatorname{dite}(q)(b(hp))(c(hp))\bigr) \,= \, \operatorname{dite}(q)\bigl(\lambda hq. \operatorname{dite}(p)(a)\bigl(b(hp,hq)\bigr)\bigr)\; \operatorname{dite}(p)(a)\bigl(c(hp,hq)\bigr) $$$
Lean4
theorem dite_dite_distrib_left {a : p → α} {b : ¬p → q → α} {c : ¬p → ¬q → α} :
(dite p a fun hp ↦ dite q (b hp) (c hp)) =
dite q (fun hq ↦ (dite p a) fun hp ↦ b hp hq) fun hq ↦ (dite p a) fun hp ↦ c hp hq :=
by split_ifs <;> rfl
