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

case neg
j : ℕ
z : String
i : ℕ
h✝ : ¬i < j
⊢ (bound_ (i + 1)).freeVarSet ⊆ (bound_ i).freeVarSet \ {free_ z}