Bug fixing of induction bugs

Allow renaming according to introduced context (Fixes #1123)
Allow induction on records (Fixes #1129)