-- Maclain Hunter: Conditional Determinism
-- Exact authored source SHA-256: 6cb8cd31364ff39227ce4abbd13e669a242c6a1bb7ba6a1cdec2c23a2553ae53
-- Machine formalization by Replit Agent; authority below Logic/Logos/God.
import Lean
namespace HunterAuthored

theorem conditional_returns_declared_branch {α : Type} (condition : Bool) (t e : α) :
    (if condition then t else e) = t ∨ (if condition then t else e) = e := by
  cases condition
  · exact Or.inr rfl
  · exact Or.inl rfl
#print axioms conditional_returns_declared_branch

end HunterAuthored