next c2_ne_c1 =>
constructor
. intro h
  apply Or.inr
  rcases h with h | h | h
  . apply Or.inl
    simp only [insert] at h
    split at h
    all_goals
      simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq] at h
      rcases h with h | h
      . exact h
      . exact False.elim $ c2_ne_c1 h
  . rw [insert_preserves_rupUnits] at h
    exact Or.inr $ Or.inl h
  . rw [insert_preserves_ratUnits] at h
    exact Or.inr $ Or.inr h
. intro h
  rcases h with h | h | h | h
  . exact False.elim $ c2_ne_c1 h
  . apply Or.inl
    simp only [insert]
    split
    all_goals
      simp only [Array.push_data, List.mem_append, List.mem_singleton, Option.some.injEq]
      exact Or.inl h
  . rw [insert_preserves_rupUnits]
    exact Or.inr $ Or.inl h
  . rw [insert_preserves_ratUnits]
    exact Or.inr $ Or.inr h
case neg
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
h✝ : ¬c2 = c1
⊢ (some c2 ∈ (f.insert c1).clauses.data ∨
      (∃ a,
          (a, false) ∈ (f.insert c1).rupUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).rupUnits.data ∧ unit (a, true) = c2) ∨
        ∃ a,
          (a, false) ∈ (f.insert c1).ratUnits.data ∧ unit (a, false) = c2 ∨
            (a, true) ∈ (f.insert c1).ratUnits.data ∧ unit (a, true) = c2) ↔
    c2 = c1 ∨
      some c2 ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c2) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c2 ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c2
no goals