cases n <;> simp [unsat, relabel, Clause.relabel]
case inr.intro
α β : Type
f : α → β
n : Nat
w : ∀ {a b : α}, mem a (List.replicate n []) → mem b (List.replicate n []) → f a = f b → a = b
⊢ (relabel f (List.replicate n [])).unsat ↔ unsat (List.replicate n [])
no goals