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