Day two working through Software Foundations with Coq. Since I like to rant, and I love Darkest Dungeon, ENTER THE DARKEST PROOF. (Please don’t sue me!)

## Naming

While trying to understand how `rewrite`

works, I come across an obvious use-case:

At this point, in current scope I have:

1 subgoals, subgoal 1 (ID 90) n : nat IHn : forall m : nat, n + S m = S (n + m) --------------- forall m : nat, S (n + S m) = S (S (n + m))Looks obvious enough. I *should* be able to substitute the `n + S m`

with `S (n + m)`

in my goal using `rewrite <- IHn`

.

# NOPE

```
Error: Found no subterm matching "n + S ?252" in the current goal.
```

Why is it: `n + S ?252`

the hypothesis clearly has `n + S m`

! Where did
`m`

go? Am I losing my marbles?

After searching around, I come across an old thread with someone getting the same error. The reply post says

The strange-looking “?738” means any term to be instantiated… Besides, rewrite cannot rewrite under a “forall”.

Is `m`

not defined? But it was up there in scope, right? Well my current scope
*did* look like: `IHn : forall m : nat, n + S m = S (n + m)`

Oh, that *does* say `forall m`

, how to make it just for that one `m`

? Well `n`

isn’t `forall`

, perhaps `intros`

?

# SUCCESS

I…. I …. don’t know what is happening.