theoreme(![A,B,C]:(inc(A,B) & inc(B,C) => inc(A,C))).
definition(inc(A,B) <=> ! [X]:(X app A => X app B)).