simp [Fitree.trigger, pair_eta]
α σ : Type
ε : σ → Type
α' σ' : Type
ε' : σ' → Type
T : Type
E : Type → Type
Δ : Dialect α' σ' ε'
e : SSAEnvE Δ T
s₁ : SSAEnv Δ
⊢ interpSSA' (Fitree.trigger e) s₁ = SSAEnvE.handle T e s₁
no goals