ANF preserves dependent types up to extensional equality. - Paulette Koronkevich; Ramon Rakow; Amal Ahmed 001; William J. Bowman (J. Funct. Program., 2022)