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

State before:
L : Type ?u.13015
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ+
f : ν ↪ IVar
h : ∀ (v : ν), f v < vars
⊢ interp (new vars f h) = fun x => True
Tactic:
ext τ
State after:
case h.a
L : Type ?u.13015
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ+
f : ν ↪ IVar
h : ∀ (v : ν), f v < vars
τ : PropAssignment ν
⊢ interp (new vars f h) τ ↔ True

State before:
case h.a
L : Type ?u.13015
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ+
f : ν ↪ IVar
h : ∀ (v : ν), f v < vars
τ : PropAssignment ν
⊢ interp (new vars f h) τ ↔ True
Tactic:
simp [new, State.new, interp, Cnf.toPropFun, PropAssignment.map_eq_map]
State after:
case h.a
L : Type ?u.13015
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ+
f : ν ↪ IVar
h : ∀ (v : ν), f v < vars
τ : PropAssignment ν
⊢ ∃ σ, τ = PropAssignment.map (⇑f) σ

State before:
case h.a
L : Type ?u.13015
ν : Type u_1
inst✝ : LitVar L ν
vars : ℕ+
f : ν ↪ IVar
h : ∀ (v : ν), f v < vars
τ : PropAssignment ν
⊢ ∃ σ, τ = PropAssignment.map (⇑f) σ
Tactic:
apply τ.exists_preimage
State after:
no goals