finished proof T_SUP
fixed T-SUP and T-STR in Type_System.v
fixed TypeSystem definition and finished proof T_STR