no goals
c : Code
k : Cont'
⊢ trStmts₁ (trNormal c k) ⊆ codeSupp' c k
cases c <;> first |rfl|exact Finset.subset_union_left _ _
case fix
k : Cont'
a✝ : Code
⊢ trStmts₁ (trNormal (Code.fix a✝) k) ⊆ codeSupp' (Code.fix a✝) k
case fix
k : Cont'
a✝ : Code
⊢ trStmts₁ (trNormal (Code.fix a✝) k) ⊆ codeSupp' (Code.fix a✝) k
rfl
no goals
case fix
k : Cont'
a✝ : Code
⊢ trStmts₁ (trNormal (Code.fix a✝) k) ⊆ codeSupp' (Code.fix a✝) k
exact Finset.subset_union_left _ _