exact c1
case s1
z : String
t : Var
x : String
c1 : ¬z = x
⊢ ¬z = x

z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}
z : String
t : Var
x : String
c1 : ¬free_ z = free_ x
s1 : (free_ x).freeVarSet \ {free_ z} = {free_ x}
⊢ (free_ x).freeVarSet ⊆ t.freeVarSet ∪ (free_ x).freeVarSet \ {free_ z}