intro v
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
⊢ ∀ (v : ν), τ (f v) = τ' (f' v)
case mp
ν : Type u_3
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
ν₁ : Type u_1
ν₂ : Type u_2
f : ν → ν₁
τ : PropAssignment ν₁
f' : ν → ν₂
τ' : PropAssignment ν₂
h : τ ∘ f = τ' ∘ f'
v : ν
⊢ τ (f v) = τ' (f' v)