λ(f : Bool → Natural)
→ λ(x : Bool)
→ (if True then f else f) (if True then x else x)