Theorem: LeanSAT.Model.PropFun.subst_distrib (LeanSAT/Model/Subst.lean)

State before:
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
⊢ subst ⟦PropForm.var v⟧ f = f v
Tactic:
ext
State after:
case a
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ subst ⟦PropForm.var v⟧ f ↔ τ✝ ⊨ f v

State before:
case a
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ subst ⟦PropForm.var v⟧ f ↔ τ✝ ⊨ f v
Tactic:
simp [PropAssignment.subst]
State after:
no goals