type Elims = [Elim]  -- ^ eliminations ordered left-to-right.