f g : Code
k : Cont'
⊢ trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
f g : Code
k : Cont'
⊢ codeSupp (Code.comp f g) k = trStmts₁ (trNormal (Code.comp f g) k) ∪ codeSupp g (Cont'.comp f k)
simp [codeSupp, codeSupp', contSupp, Finset.union_assoc]
no goals
f g : Code
k : Cont'
⊢ trStmts₁ (trNormal g (Cont'.comp f k)) ∪
      (codeSupp' g (Cont'.comp f k) ∪ (trStmts₁ (trNormal f k) ∪ (codeSupp' f k ∪ contSupp k))) =
    trStmts₁ (trNormal g (Cont'.comp f k)) ∪ (codeSupp' g (Cont'.comp f k) ∪ (codeSupp' f k ∪ contSupp k))
rw [← Finset.union_assoc _ _ (contSupp k),
  Finset.union_eq_right_iff_subset.2 (codeSupp'_self _ _)]