Theorem: denoteTypedArgs_equiv (MLIR/Semantics/Semantics.lean)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
args : TypedArgs Δ
⊢ ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs args vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs args vals env₂ = Except.ok (r, env₂')
Tactic:
induction args
State after:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs [] vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ → ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs [] vals env₂ = Except.ok (r, env₂')

case cons
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head✝ : TypedArg Δ
tail✝ : List (TypedArg Δ)
tail_ih✝ :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs tail✝ vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs tail✝ vals env₂ = Except.ok (r, env₂')
⊢ ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs (head✝ :: tail✝) vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (head✝ :: tail✝) vals env₂ = Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs [] vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ → ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs [] vals env₂ = Except.ok (r, env₂')
Tactic:
case nil =>
  intros val env₁ r env₁' H env₂ Henv₂
  simp [denoteTypedArgs] at *
  exists env₂
  simp_monad at *; subst H; assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
⊢ ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs (argsHead :: argsTail) vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) vals env₂ = Except.ok (r, env₂')
Tactic:
case cons argsHead argsTail HInd =>
  intros vals env₁ r env₁' H env₂ Henv₂
  have ⟨valsHead, valsTail, HVals, HHead, HTail⟩ := denoteTypedArgs_cons_args H
  subst vals
  have HHead₂ := TopM.set_equiv Henv₂ HHead
  specialize (HInd HTail (by apply SSAEnv.equiv_set Henv₂))
  have ⟨env₂', Hequiv₂', Henv₂'⟩ := HInd
  exists env₂'
  cases r
  rw [denoteTypedArgs_cons_unfold]
  simp_monad
  rw [HHead₂]; simp; rw [Henv₂']
  simp; assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs [] vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ → ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs [] vals env₂ = Except.ok (r, env₂')
Tactic:
intros val env₁ r env₁' H env₂ Henv₂
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : denoteTypedArgs [] val env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs [] val env₂ = Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : denoteTypedArgs [] val env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs [] val env₂ = Except.ok (r, env₂')
Tactic:
simp [denoteTypedArgs] at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : pure () env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ pure () env₂ = Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : pure () env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ pure () env₂ = Except.ok (r, env₂')
Tactic:
exists env₂
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : pure () env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ SSAEnv.equiv env₁' env₂ ∧ pure () env₂ = Except.ok (r, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : pure () env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ SSAEnv.equiv env₁' env₂ ∧ pure () env₂ = Except.ok (r, env₂)
Tactic:
simp_monad at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
H : env₁ = env₁'
⊢ SSAEnv.equiv env₁' env₂

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
H : env₁ = env₁'
⊢ SSAEnv.equiv env₁' env₂
Tactic:
subst H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ SSAEnv.equiv env₁ env₂

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ SSAEnv.equiv env₁ env₂
Tactic:
assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
⊢ ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs (argsHead :: argsTail) vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) vals env₂ = Except.ok (r, env₂')
Tactic:
intros vals env₁ r env₁' H env₂ Henv₂
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
vals : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : denoteTypedArgs (argsHead :: argsTail) vals env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) vals env₂ = Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
vals : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : denoteTypedArgs (argsHead :: argsTail) vals env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) vals env₂ = Except.ok (r, env₂')
Tactic:
have ⟨valsHead, valsTail, HVals, HHead, HTail⟩ := denoteTypedArgs_cons_args H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
vals : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : denoteTypedArgs (argsHead :: argsTail) vals env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HVals : vals = valsHead :: valsTail
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) vals env₂ = Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
vals : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : denoteTypedArgs (argsHead :: argsTail) vals env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HVals : vals = valsHead :: valsTail
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) vals env₂ = Except.ok (r, env₂')
Tactic:
subst vals
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Tactic:
have HHead₂ := TopM.set_equiv Henv₂ HHead
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Tactic:
specialize (HInd HTail (by apply SSAEnv.equiv_set Henv₂))
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Tactic:
have ⟨env₂', Hequiv₂', Henv₂'⟩ := HInd
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Tactic:
exists env₂'
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
⊢ SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
⊢ SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Tactic:
cases r
State after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (PUnit.unit, env₂')

State before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (PUnit.unit, env₂')
Tactic:
rw [denoteTypedArgs_cons_unfold]
State after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    bind (TopM.set argsHead.fst valsHead argsHead.snd) (fun x => denoteTypedArgs argsTail valsTail) env₂ =
      Except.ok (PUnit.unit, env₂')

State before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    bind (TopM.set argsHead.fst valsHead argsHead.snd) (fun x => denoteTypedArgs argsTail valsTail) env₂ =
      Except.ok (PUnit.unit, env₂')
Tactic:
simp_monad
State after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    (match TopM.set argsHead.fst valsHead argsHead.snd env₂ with
      | Except.error err => Except.error err
      | Except.ok v => denoteTypedArgs argsTail valsTail v.snd) =
      Except.ok (PUnit.unit, env₂')

State before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    (match TopM.set argsHead.fst valsHead argsHead.snd env₂ with
      | Except.error err => Except.error err
      | Except.ok v => denoteTypedArgs argsTail valsTail v.snd) =
      Except.ok (PUnit.unit, env₂')
Tactic:
rw [HHead₂]
State after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    (match Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) with
      | Except.error err => Except.error err
      | Except.ok v => denoteTypedArgs argsTail valsTail v.snd) =
      Except.ok (PUnit.unit, env₂')

State before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    (match Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) with
      | Except.error err => Except.error err
      | Except.ok v => denoteTypedArgs argsTail valsTail v.snd) =
      Except.ok (PUnit.unit, env₂')
Tactic:
simp
State after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) =
      Except.ok (PUnit.unit, env₂')

State before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) =
      Except.ok (PUnit.unit, env₂')
Tactic:
rw [Henv₂']
State after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧ Except.ok ((), env₂') = Except.ok (PUnit.unit, env₂')

State before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧ Except.ok ((), env₂') = Except.ok (PUnit.unit, env₂')
Tactic:
simp
State after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂'

State before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂'
Tactic:
assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
⊢ SSAEnv.equiv (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) ?m.958985
Tactic:
apply SSAEnv.equiv_set Henv₂
State after:
no goals