the Sorts of C . I = INT by AOFA_A00:55;
hence t value_at (C,u) is integer ; :: thesis: verum