simp only [isUnit, Prod.forall, toList]
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ c.isUnit = some l ↔ c.toList = [l]
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ (match c.clause with
      | [l] => some l
      | x => none) =
      some l ↔
    c.clause = [l]