exfalso
case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ evaluate M v (~⌈⌈α✝ :: γs✝⌉⌉ξ)
case consComp
W : Type
M : KripkeModel W
v : W
ξ : Formula
α✝ : Program
Fs✝ : List Formula
v1✝ : W
ηs✝ γs✝ : List Program
a✝⁴ : ℕ
a✝³ : (Fs✝, (·a✝⁴) :: ηs✝) ∈ H α✝
a✝² : M.Rel a✝⁴ v v1✝
a✝¹ : evaluate M v (Con Fs✝)
a✝ : witness M v1✝ (ηs✝ ++ γs✝) ξ
def_n : (witness.consComp a✝² a✝³ a✝¹ a✝).length = 0
⊢ False