proposition: Theorem FVSSubst: fv (tSSubst a s) =$= (fv a -- Dom s) ++ fvr (keepFirst s (fv a)).
proof: Proof. unfold tSSubst. addRenSpec. apply alpha_preserves_free_vars in Hala. rw Hala. apply free_vars_SSubstAux. trivial. Qed.
imports: SubstAuxAlphaEq AlphaRen Term