■

data Bool : Set0
  where
    true : Bool
    false : Bool

data BoolHold : Bool -> Set0
  where
    boolHold : (b1 : Bool) -> BoolHold b1

not : Bool -> Bool
not b2 with b2
... | true = false
... | false = true

g : (b : Bool) -> BoolHold (not b)
g b with b
g b | true with not b
g b | true | true = boolHold false -- 凄いね！！
g b | true | false = boolHold false
g b | false with not b
g b | false | true = boolHold true
g b | false | false = boolHold true -- 凄いね！！

凄いね！！