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:

```
Theorem adding_n_Sm : forall n m : nat,
n + S m = S n + m.
Proof.
intros n.
induction n.
simpl. reflexivity.
simpl. rewrite <- IHn.
```

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`

?

```
Theorem adding_n_Sm : forall n m : nat,
n + S m = S n + m.
Proof.
intros n m.
induction n.
simpl. reflexivity.
simpl. rewrite <- IHn.
```

# SUCCESS

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