no goals
case ret
k✝ : Cont'
⊢ Λ'.ret k✝ ∈ trStmts₁ (Λ'.ret k✝)
first |apply Finset.mem_singleton_self|apply Finset.mem_insert_self
no goals
case ret
k✝ : Cont'
⊢ Λ'.ret k✝ ∈ trStmts₁ (Λ'.ret k✝)
apply Finset.mem_singleton_self
no goals
case pred
q₁✝ q₂✝ : Λ'
q₁_ih✝ : q₁✝ ∈ trStmts₁ q₁✝
q₂_ih✝ : q₂✝ ∈ trStmts₁ q₂✝
⊢ Λ'.pred q₁✝ q₂✝ ∈ trStmts₁ (Λ'.pred q₁✝ q₂✝)
apply Finset.mem_insert_self