related ssubst_bterm to ssubst_bterm_aux.
related ssubst_bterm to ssubst_bterm_aux.

the proof was already done as a part of a different lemma. now used mutual induction to give a name to this part as well.

aa755/SquiggleEq,aa755/SquiggleEq