A formalization of System I with type Top in Agda. - Agustín Séttimo; Cristian Sottile; Cecilia Manzino (CoRR, 2026)