quantities in case don't need to be *exactly* the same

...as long as they are all compatible with the target.
for example, given ω.n : ℕ:
```
  case double_it? return ℕ of {
    'true  ⇒ plus n n;
    'false ⇒ n
  }
```

lib/Quox/Typechecker.idr

@@ -5,6 +5,7 @@ import public Quox.Equal
 
 import Data.List
 import Data.SnocVect
+import Data.List1
 
 %default total
 
@@ -18,16 +19,28 @@ public export
 CanTC q = CanTC' q IsGlobal
 
 
-private
+export
 popQs : HasErr q m => IsQty q =>
         QOutput q s -> QOutput q (s + n) -> m (QOutput q n)
 popQs [<]         qout         = pure qout
 popQs (pis :< pi) (qout :< rh) = do expectCompatQ rh pi; popQs pis qout
 
-private %inline
+export %inline
 popQ : HasErr q m => IsQty q => q -> QOutput q (S n) -> m (QOutput q n)
 popQ pi = popQs [< pi]
 
+export
+lubs1 : IsQty q => List1 (QOutput q n) -> Maybe (QOutput q n)
+lubs1 ([<] ::: _) = Just [<]
+lubs1 ((qs :< p) ::: pqs) =
+  let (qss, ps) = unzip $ map unsnoc pqs in
+  [|lubs1 (qs ::: qss) :< foldlM lub p ps|]
+
+export
+lubs : IsQty q => TyContext q d n -> List (QOutput q n) -> Maybe (QOutput q n)
+lubs ctx []        = Just $ zeroFor ctx
+lubs ctx (x :: xs) = lubs1 $ x ::: xs
+
 
 parameters {auto _ : IsQty q} {auto _ : CanTC q m}
  mutual
@@ -329,19 +342,13 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     unless (ttags == armTags) $ throwError $ BadCaseEnum ttags armTags
     armres <- for arms $ \(a, s) =>
       checkC ctx sg s (sub1 ret (Tag a :# tres.type))
-    armout <- allEqual (zip armres arms)
-    -- then Ψ | Γ ⊢ σ · case ⋯ ⇒ ret[t/x] ⊳ πΣ₁ + Σ₂
+    let Just armout = lubs ctx armres
+          | _ => throwError $ BadCaseQtys ctx $
+              zipWith (\qs, (t, rhs) => (qs, Tag t)) armres arms
     pure $ InfRes {
       type = sub1 ret t,
       qout = pi * tres.qout + armout
     }
-   where
-    allEqual : List (QOutput q n, TagVal, Term q d n) -> m (QOutput q n)
-    allEqual [] = pure $ zeroFor ctx
-    allEqual lst@((x, _) :: xs) =
-      if all (\y => x == fst y) xs then pure x
-      else throwError $ BadCaseQtys ctx $
-             map (\(qs, t, s) => (qs, Tag t, s)) lst
 
   infer' ctx sg (CaseNat pi pi' n ret zer suc) = do
     -- if 1 ≤ π
@@ -354,30 +361,29 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ ⊢ σ · zer ⇐ A[0 ∷ ℕ/n] ⊳ Σz
     zerout <- checkC ctx sg zer (sub1 ret (Zero :# Nat))
     -- if Ψ | Γ, n : ℕ, ih : A ⊢ σ · suc ⇐ A[succ p ∷ ℕ/n] ⊳ Σs, ρ₁.p, ρ₂.ih
-    -- with Σz = Σs, (ρ₁ + ρ₂) ≤ πσ
+    -- with ρ₂ ≤ π'σ, (ρ₁ + ρ₂) ≤ πσ
     let [< p, ih] = suc.names
         pisg      = pi * sg.fst
         sucCtx    = extendTyN [< (pisg, p, Nat), (pi', ih, ret.term)] ctx
         sucType   = substCaseNatRet ret
     sucout :< qp :< qih <- checkC sucCtx sg suc.term sucType
-    unless (zerout == sucout) $ do
-      let sucp = Succ $ FT $ unq p
-          suc  = subN suc [< F $ unq p, F $ unq ih]
-      throwError $ BadCaseQtys ctx [(zerout, Zero, zer), (sucout, sucp, suc)]
-    expectCompatQ qih pi'
+    let Just armout = lubs ctx [zerout, sucout]
+          | _ => throwError $ BadCaseQtys ctx $
+              [(zerout, Zero), (sucout, Succ $ FT $ unq p)]
+    expectCompatQ qih (pi' * sg.fst)
     -- [fixme] better error here
     expectCompatQ (qp + qih) pisg
-    -- then Ψ | Γ ⊢ case ⋯ ⇒ A[n] ⊳ πΣn + Σz
+    -- then Ψ | Γ ⊢ case ⋯ ⇒ A[n] ⊳ πΣn + (Σz ∧ Σs)
     pure $ InfRes {
       type = sub1 ret n,
-      qout = pi * nres.qout + zerout
+      qout = pi * nres.qout + armout
     }
 
   infer' ctx sg (fun :% dim) = do
-    -- if Ψ | Γ ⊢ σ · f ⇒ Eq [i ⇒ A] l r ⊳ Σ
+    -- if Ψ | Γ ⊢ σ · f ⇒ Eq [𝑖 ⇒ A] l r ⊳ Σ
     InfRes {type, qout} <- inferC ctx sg fun
     ty <- fst <$> expectEq !ask ctx type
-    -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p› ⊳ Σ
+    -- then Ψ | Γ ⊢ σ · f p ⇒ A‹p/𝑖› ⊳ Σ
     pure $ InfRes {type = dsub1 ty dim, qout}
 
   infer' ctx sg (term :# type) = do