...but at least I now know a little bit more about `Prop`, `Bool`, and `Dec`.

**Question**. Suppose

```agda
∀ i → Dec (f i ≈ g i)
```

and suppose we define

```agda
f ≐ g = ∀ i → f i ≈ g i
```

Can we then prove `Dec (f ≐ g)`?

(That's what we need in the hole on line 142, and that what I'm trying to do in
lines 129--134.  I have the `Bool` part, but I still need the `Reflects (f ≐ g)` part.)