English
For any P, A, B, and C with appropriate decidability, the equality dite P A B = dite P A B is always either equal to A h or B h for some h; more precisely, dite_eq_or_eq states that (∃ h, dite P A B = A h) ∨ (∃ h, dite P A B = B h).
Русский
Для любых P, A, B, C с надлежащей дискайтабельностью, тождественно dite P A B совпадает либо с A h для некоторого h, либо с B h для некоторого h; точнее: существует либо h, такое что dite P A B = A h, либо h, такое что dite P A B = B h.
LaTeX
$$$\big(\exists h, \; \operatorname{dite} P A B = A h\big) \;\lor\; \big(\exists h, \operatorname{dite} P A B = B h\big)$$$
Lean4
theorem dite_eq_or_eq : (∃ h, dite P A B = A h) ∨ ∃ h, dite P A B = B h :=
if h : _ then .inl ⟨h, dif_pos h⟩ else .inr ⟨h, dif_neg h⟩
