s/ih/Ai.
Removed unnecessary ATP hypothesis.
s/∃ (λ x → .../∃[ x ] ...
Added +-comm using an instance of the induction principle.
Working on the equivalence of the induction principles of N.