split
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ (match c.clause with
      | [l] => some l
      | x => none) =
      some l ↔
    c.clause = [l]
case h_1
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝ : List (Literal (PosFin n))
l✝ : Literal (PosFin n)
heq✝ : c.clause = [l✝]
⊢ some l✝ = some l ↔ c.clause = [l]

case h_2
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
x✝¹ : List (Literal (PosFin n))
x✝ : ∀ (l : Literal (PosFin n)), c.clause = [l] → False
⊢ none = some l ↔ c.clause = [l]