Theorem: interpSSA'_trigger_MemberSumL (MLIR/Semantics/SSAEnv.lean)

State before:
α σ : 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₁
Tactic:
simp [Fitree.trigger, pair_eta]
State after:
no goals