Hello,

I am trying to solve this Exercise

#### Exercise: 3 stars, standard (STLCE_definitions)

from this Chapter

https://softwarefoundations.cis.upenn.edu/plf-current/MoreStlc.html

Having problems with definition of term `let`

in Fixpoint subst.

This is how I defined it.

```
Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
match t with
....
| tlet y t t' =>
if eqb_string x y then (tlet y s t')
else (tlet y (subst x s t) (subst x s t'))
...
end.
Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).
```

This is what I think about it:

Substitution and let are common in sense that they replace only unbound variables with new term in both cases.

so if `x`

and `y`

are the same string, in final term only s will replace corresponding unbound variables.

and if they are different, then let should work and replace all free occurrences of y with t in t’ . And let should work after substitution will work and will replace all occurrences of x with s in both terms

which participate in let : in t and t’

Please advice. I couldn’t prove LET part in 2 final theorems in this chapter… looks like because of wrong definition of let in Fixpoint subst.

I also tried this definition

```
Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
match t with
....
| tlet y t t' => tlet y (subst x s t) (subst x s t')
...
end.
Notation "'[' x ':=' s ']' t" := (subst x s t) (at level 20).
```

But with this definition theorems also do not work for let.

Thanks,

Nat