Ind1

type t
interpret t -> int

function sum(X:t) : t

definition {
    sum(X:t) = 0 if X <= 0 else (X + sum(X-1))
}
proof {
    apply rec[t]
}

property sum(Y) >= Y
proof {
    apply ind[t] with X = Y;
    showgoals;
    assume sum with X = Y;
    defergoal;
    assume sum with X = Y + 1;
    showgoals
}