for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}.
interpretation "countable_union" 'big_union η.t = (countable_union ? t).
for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}.
interpretation "countable_union" 'big_union η.t = (countable_union ? t).