module ExtendedLam where data Bool : Set where false : Bool true : Bool f : Bool → Bool → Bool f = λ { x false → true ; y true → y }