ANF preserves dependent types up to extensional equality