intro W M w
case refine_2
α : Program
ℓ : TP α
⊢ Con (F α ℓ)⋀signature α ℓ≡signature α ℓ
case refine_2
α : Program
ℓ : TP α
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (Con (F α ℓ)⋀signature α ℓ) ↔ evaluate M w (signature α ℓ)