The definition of Int says that if n has type int them Int n has type int term.
The definition of Add (the constructor) says that Add (the expression) has type (int -> int -> int) term.
The definition of App says that if f has type ('b -> 'a) term and x has type 'b term (for some 'a and 'b) then App (f, x) has type 'a term.

So Int 1 has type int term (first rule)
And in the third rule, replacing f by Add and x by Int 1 (using int for b and int -> int for 'a) we get that App (f, x) (ie App (Add, Int 1)) has type (int -> int) term.

(int -> int -> int is the same as (int -> (int -> int))

Hi,
Emillon gave you an answer to your question, and I will not add to his answer. However there is another examples of GADT that you may want to check out : https://www.zapashcanon.fr/ocaml
Just scroll down to the â€śGADTâ€ť section.

App (Add, Int 1) is of type (int -> int) term for the same reason that (+) 1 is of type int -> int.
And yes the -> operator is right-associative (because application is left-associative).