split_ifs
j : ℕ
z x : String
⊢ (if free_ x = free_ z then bound_ j else free_ x).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}
case pos
j : ℕ
z x : String
h✝ : free_ x = free_ z
⊢ (bound_ j).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}

case neg
j : ℕ
z x : String
h✝ : ¬free_ x = free_ z
⊢ (free_ x).freeVarSet ⊆ (free_ x).freeVarSet \ {free_ z}