split <;> rename_i a_lt
case isTrue.w
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
⊢ ((if w : a < g.numLiterals then ⟨a, w⟩ else ⟨0, ⋯⟩) = if w : b < g.numLiterals then ⟨b, w⟩ else ⟨0, ⋯⟩) → a = b
case isTrue.w.isTrue
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
a_lt : a < g.numLiterals
⊢ ⟨a, a_lt⟩ = ⟨b, mb⟩ → a = b

case isTrue.w.isFalse
g : CNF Nat
h : ∃ a, mem a g
a b : Nat
ma : a < g.numLiterals
mb : b < g.numLiterals
a_lt : ¬a < g.numLiterals
⊢ ⟨a, ma⟩ = ⟨b, mb⟩ → a = b