IME unwrapping usually comes from the variant of an enum being determined by the ambient invariants in the program. For example, if you have a dependent pair, (

IME unwrapping usually comes from the variant of an enum being determined by the ambient invariants in the program. For example, if you have a dependent pair, (x,y), x determines the variant of y. Similar consideration for switching between a array of options of pairs and a pair of arrays of options. The simplest example of this is array subscripting. A sufficient bound on n will determine the variant of arr.get(n). The API acknowledges this common case by providing arr[n].