no goals
fs : Code
k : Cont'
⊢ contSupp (Cont'.cons₁ fs k) =
    trStmts₁
        (move₂ (fun x => false) main aux
          (move₂ (fun s => decide (s = Γ'.consₗ)) stack main
            (move₂ (fun x => false) aux stack (trNormal fs (Cont'.cons₂ k))))) ∪
      codeSupp fs (Cont'.cons₂ k)
simp [codeSupp, codeSupp', contSupp, Finset.union_assoc]