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

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ denoteRegionsEquivInvariant regions →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx regions idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (res, env₂')
Tactic:
induction regions <;> intros H idx args env res env' Hrun env₂ Henv₂ <;> try contradiction
State after:
case cons
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head✝ : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail✝ : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
tail_ih✝ :
  denoteRegionsEquivInvariant tail✝ →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail✝ idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail✝ idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head✝ :: tail✝)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head✝ :: tail✝) idx args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head✝ :: tail✝) idx args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) idx args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) idx args env₂ = Except.ok (res, env₂')
Tactic:
case cons head tail HInd =>
  cases idx
  case zero =>
    simp at *
    specialize (H (by constructor) (by assumption) (by assumption))
    assumption
  case succ idx' =>
    specialize (HInd (by
      intros region Hregions args env res env' Hrun env₂ Henv₂
      specialize (H (.tail _ Hregions) (by assumption) (by assumption))
      assumption
    ))
    simp at Hrun
    specialize (HInd Hrun Henv₂)
    assumption
State after:
no goals

State before:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
H : denoteRegionsEquivInvariant []
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx [] idx args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx [] idx args env₂ = Except.ok (res, env₂')
Tactic:
contradiction
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) idx args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) idx args env₂ = Except.ok (res, env₂')
Tactic:
cases idx
State after:
case zero
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) Nat.zero args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) Nat.zero args env₂ = Except.ok (res, env₂')

case succ
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
n✝ : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ n✝) args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ n✝) args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) Nat.zero args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) Nat.zero args env₂ = Except.ok (res, env₂')
Tactic:
case zero =>
  simp at *
  specialize (H (by constructor) (by assumption) (by assumption))
  assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')
Tactic:
case succ idx' =>
  specialize (HInd (by
    intros region Hregions args env res env' Hrun env₂ Henv₂
    specialize (H (.tail _ Hregions) (by assumption) (by assumption))
    assumption
  ))
  simp at Hrun
  specialize (HInd Hrun Henv₂)
  assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) Nat.zero args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) Nat.zero args env₂ = Except.ok (res, env₂')
Tactic:
simp at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) 0 args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) 0 args env₂ = Except.ok (res, env₂')
Tactic:
specialize (H (by constructor) (by assumption) (by assumption))
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
H : ∃ env₂', SSAEnv.equiv env' env₂' ∧ head args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) 0 args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
H : ∃ env₂', SSAEnv.equiv env' env₂' ∧ head args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) 0 args env₂ = Except.ok (res, env₂')
Tactic:
assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ ?m.1012060 ∈ head :: tail
Tactic:
constructor
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ head ?m.1012062 ?m.1012063 = Except.ok (?m.1012064, ?m.1012065)
Tactic:
assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ SSAEnv.equiv env ?m.1012067
Tactic:
assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')
Tactic:
specialize (HInd (by
  intros region Hregions args env res env' Hrun env₂ Henv₂
  specialize (H (.tail _ Hregions) (by assumption) (by assumption))
  assumption
))
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
HInd :
  ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
HInd :
  ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')
Tactic:
specialize (HInd Hrun Henv₂)
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
HInd : ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx' args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
HInd : ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx' args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')
Tactic:
assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
⊢ denoteRegionsEquivInvariant tail
Tactic:
intros region Hregions args env res env' Hrun env₂ Henv₂
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
idx' : ℕ
Hrun✝ : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args✝ env✝ = Except.ok (res✝, env'✝)
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
Hregions : region ∈ tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
idx' : ℕ
Hrun✝ : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args✝ env✝ = Except.ok (res✝, env'✝)
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
Hregions : region ∈ tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
specialize (H (.tail _ Hregions) (by assumption) (by assumption))
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
idx' : ℕ
Hrun✝ : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args✝ env✝ = Except.ok (res✝, env'✝)
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
Hregions : region ∈ tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
idx' : ℕ
Hrun✝ : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args✝ env✝ = Except.ok (res✝, env'✝)
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
Hregions : region ∈ tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
idx' : ℕ
Hrun✝ : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args✝ env✝ = Except.ok (res✝, env'✝)
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
Hregions : region ∈ tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ region ?m.1012165 ?m.1012166 = Except.ok (?m.1012167, ?m.1012168)
Tactic:
assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
idx' : ℕ
Hrun✝ : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args✝ env✝ = Except.ok (res✝, env'✝)
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
Hregions : region ∈ tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ SSAEnv.equiv env ?m.1012170
Tactic:
assumption
State after:
no goals