Fix induction so proof scripts work
Fix extensionalityR