Definition maybe_return (A: Type) (a: nat) (b: nat) (d: A) :=
  match (Nat.eqb a b) with
  | true => Some d
  | false => None
end.