int_add@{} (x y : Int) : Int. Proof. induction x as [|x IHx|x IHx] in y |- *. - exact y. - exact (int_succ (IHx y)). - exact (int_pred (IHx y)). Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.