using induction on a hypothesis causes loss of information

[stilltracy]

This issue arose in the proof of legal_tids_steps, and instrument_sim_safe': after doing an induction on Hsteps and Hstep, the base case looks unprovable. @mansky1

[mansky1]

When doing induction on a term that has (Some P) in a position instead of just a variable, you have to use remember (and sometimes generalize dependent) to retain the relevant information. I've checked in an example of its use at the beginning of legal_tids_steps.