split_ifs
j : ℕ
zs : List String
i : ℕ
⊢ (if i < j then bound_ i
      else
        if x : i - j < (List.map free_ zs).length then (List.map free_ zs)[i - j]
        else bound_ (i - j - (List.map free_ zs).length + j)).freeVarSet ⊆
    (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset
case pos
j : ℕ
zs : List String
i : ℕ
h✝ : i < j
⊢ (bound_ i).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset

case pos
j : ℕ
zs : List String
i : ℕ
h✝¹ : ¬i < j
h✝ : i - j < (List.map free_ zs).length
⊢ (List.map free_ zs)[i - j].freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset

case neg
j : ℕ
zs : List String
i : ℕ
h✝¹ : ¬i < j
h✝ : ¬i - j < (List.map free_ zs).length
⊢ (bound_ (i - j - (List.map free_ zs).length + j)).freeVarSet ⊆ (bound_ i).freeVarSet ∪ (List.map free_ zs).toFinset