T @--> is strongly-normalizing with_UN_property with_Church-Rosser_property Relation by Th70, Th78;
hence nf t,(T @--> ) is type of T by Th76; :: thesis: verum