feat: propagation for functions with singleton domain in `grind`

This PR adds propagation rules for functions that take singleton
types. This feature is useful for discharging verification conditions
produced by `mvcgen`. For example:

```lean
example (h : (fun (_ : Unit) => x + 1) = (fun _ => 1 + y)) : x = y := by
  grind
```