Theorem: LeanSAT.Encode.EncCNF.LawfulState.interp_new' (LeanSAT/Encode/EncCNF.lean)

State before:
L : Type ?u.18246
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ
f : ν ↪ Fin vars
⊢ interp (new' vars f) = fun x => True
Tactic:
simp [new']
State after:
no goals