. intro _
  exact Or.inl c2_eq_c1
case mp
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : 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

case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
⊢ (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) →
    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
case mpr
n : Nat
f : DefaultFormula n
c1 c2 : DefaultClause n
c2_eq_c1 : c2 = c1
⊢ (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) →
    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