updating STac proofs to track well-formed subst.

- Apply is not sound right now because of how substitutions work.
- Solving this may require some serious changes.