やる気！！！

でません・・・。

natEq : Nat -> Nat -> Bool
natEq zero zero = true
natEq zero (succ b) = false
natEq (succ a) zero = false
natEq (succ a) (succ b) = natEq a b

boolEq : Bool -> Bool -> Bool
boolEq true true = true
boolEq false false = true
boolEq _ _ = false

valueSame : {A : Set0} {p : A -> A -> Bool} -> (a : A) -> (b : A) -> Val (p a b)
valueSame {Nat} a b = val (natEq a b)
valueSame {Bool} a b = val (boolEq a b)
valueSame {_} _ _ = val false

とかダメなんですかね・・・。