contradiction
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : x' = z
h1 : ¬occursFreeIn (free_ x') F
⊢ V (free_ x') = d
no goals