split_ifs
j : ℕ
z : String
i : ℕ
⊢ (if i < j then bound_ i else if i = j then free_ z 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 pos
j : ℕ
z : String
i : ℕ
h✝¹ : ¬i < j
h✝ : i = j
⊢ (free_ z).freeVarSet ⊆ (bound_ i).freeVarSet ∪ {free_ z}

case neg
j : ℕ
z : String
i : ℕ
h✝¹ : ¬i < j
h✝ : ¬i = j
⊢ (bound_ (i - 1)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ {free_ z}