K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l' : Λ'
h : l' ∈ trSupp M S
⊢ ∀ (q : Stmt₂),
    TM2.SupportsStmt S q →
      (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
          ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l' : Λ'
h : l' ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M l')
suffices ∀ (q) (_ : TM2.SupportsStmt S q) (_ : ∀ x ∈ trStmts₁ q, x ∈ trSupp M S),
    TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
    ∀ l' ∈ trStmts₁ q, TM1.SupportsStmt (trSupp M S) (tr M l') by
  rcases Finset.mem_biUnion.1 h with ⟨l, lS, h⟩
  have :=
    this _ (ss.2 l lS) fun x hx ↦ Finset.mem_biUnion.2 ⟨_, lS, Finset.mem_insert_of_mem hx⟩
  rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ h]
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (q : Stmt₂),
    TM2.SupportsStmt S q →
      (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
          ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l' : Λ'
h : l' ∈ trSupp M S
⊢ ∀ (q : Stmt₂),
    TM2.SupportsStmt S q →
      (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
          ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')
clear h l'
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (k : K) (s : StAct k) (q : Stmt₂),
    (TM2.SupportsStmt S q →
        (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
            ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')) →
      TM2.SupportsStmt S (stRun s q) →
        (∀ (x : Λ'), x ∈ trStmts₁ (stRun s q) → x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q)) ∧
            ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q) → TM1.SupportsStmt (trSupp M S) (tr M l')

case refine'_2
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (a : σ → σ) (q : Stmt₂),
    (TM2.SupportsStmt S q →
        (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
            ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')) →
      TM2.SupportsStmt S (TM2.Stmt.load a q) →
        (∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.load a q) → x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a q)) ∧
            ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.load a q) → TM1.SupportsStmt (trSupp M S) (tr M l')

case refine'_3
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (p : σ → Bool) (q₁ q₂ : Stmt₂),
    (TM2.SupportsStmt S q₁ →
        (∀ (x : Λ'), x ∈ trStmts₁ q₁ → x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q₁) ∧
            ∀ (l' : Λ'), l' ∈ trStmts₁ q₁ → TM1.SupportsStmt (trSupp M S) (tr M l')) →
      (TM2.SupportsStmt S q₂ →
          (∀ (x : Λ'), x ∈ trStmts₁ q₂ → x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal q₂) ∧
              ∀ (l' : Λ'), l' ∈ trStmts₁ q₂ → TM1.SupportsStmt (trSupp M S) (tr M l')) →
        TM2.SupportsStmt S (TM2.Stmt.branch p q₁ q₂) →
          (∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.branch p q₁ q₂) → x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p q₁ q₂)) ∧
              ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.branch p q₁ q₂) → TM1.SupportsStmt (trSupp M S) (tr M l')

case refine'_4
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (l : σ → Λ),
    TM2.SupportsStmt S (TM2.Stmt.goto l) →
      (∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.goto l) → x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l)) ∧
          ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.goto l) → TM1.SupportsStmt (trSupp M S) (tr M l')

case refine'_5
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ TM2.SupportsStmt S TM2.Stmt.halt →
    (∀ (x : Λ'), x ∈ trStmts₁ TM2.Stmt.halt → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ TM2.Stmt.halt → TM1.SupportsStmt (trSupp M S) (tr M l')
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (q : Stmt₂),
    TM2.SupportsStmt S q →
      (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
          ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')
refine' stmtStRec _ _ _ _ _
case intro.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l' : Λ'
h✝ : l' ∈ trSupp M S
this :
  ∀ (q : Stmt₂),
    TM2.SupportsStmt S q →
      (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
          ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ
lS : l ∈ S
h : l' ∈ insert (normal l) (trStmts₁ (M l))
⊢ TM1.SupportsStmt (trSupp M S) (tr M l')
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l' : Λ'
h : l' ∈ trSupp M S
this :
  ∀ (q : Stmt₂),
    TM2.SupportsStmt S q →
      (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
          ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M l')
rcases Finset.mem_biUnion.1 h with ⟨l, lS, h⟩
case intro.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l' : Λ'
h✝ : l' ∈ trSupp M S
this✝ :
  ∀ (q : Stmt₂),
    TM2.SupportsStmt S q →
      (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
          ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ
lS : l ∈ S
h : l' ∈ insert (normal l) (trStmts₁ (M l))
this :
  TM1.SupportsStmt (trSupp M S) (trNormal (M l)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (M l) → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M l')
case intro.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l' : Λ'
h✝ : l' ∈ trSupp M S
this :
  ∀ (q : Stmt₂),
    TM2.SupportsStmt S q →
      (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
          ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ
lS : l ∈ S
h : l' ∈ insert (normal l) (trStmts₁ (M l))
⊢ TM1.SupportsStmt (trSupp M S) (tr M l')
have :=
  this _ (ss.2 l lS) fun x hx ↦ Finset.mem_biUnion.2 ⟨_, lS, Finset.mem_insert_of_mem hx⟩
no goals
case intro.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l' : Λ'
h✝ : l' ∈ trSupp M S
this✝ :
  ∀ (q : Stmt₂),
    TM2.SupportsStmt S q →
      (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
          ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ
lS : l ∈ S
h : l' ∈ insert (normal l) (trStmts₁ (M l))
this :
  TM1.SupportsStmt (trSupp M S) (trNormal (M l)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (M l) → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M l')
rcases Finset.mem_insert.1 h with (rfl | h) <;> [exact this.1; exact this.2 _ h]
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (stRun s q✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ (stRun s q✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (k : K) (s : StAct k) (q : Stmt₂),
    (TM2.SupportsStmt S q →
        (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
            ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')) →
      TM2.SupportsStmt S (stRun s q) →
        (∀ (x : Λ'), x ∈ trStmts₁ (stRun s q) → x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q)) ∧
            ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q) → TM1.SupportsStmt (trSupp M S) (tr M l')
intro _ s _ IH ss' sub
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), x ∈ trStmts₁ (stRun s q✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (stRun s q✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ (stRun s q✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
rw [TM2to1.supports_run] at ss'
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), x ∈ trStmts₁ (stRun s q✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
simp only [TM2to1.trStmts₁_run, Finset.mem_union, Finset.mem_insert, Finset.mem_singleton]
  at sub
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
have hgo := sub _ (Or.inl <| Or.inl rfl)
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
have hret := sub _ (Or.inl <| Or.inr rfl)
case refine'_1.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_1
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
cases' IH ss' fun x hx ↦ sub x <| Or.inr hx with IH₁ IH₂
case refine'_1.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : l ∈ trStmts₁ (stRun s q✝)
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
case refine'_1.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (stRun s q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
refine' ⟨by simp only [trNormal_run, TM1.SupportsStmt]; intros; exact hgo, fun l h ↦ _⟩
case refine'_1.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : l ∈ {go k✝ s q✝, ret q✝} ∪ trStmts₁ q✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
case refine'_1.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : l ∈ trStmts₁ (stRun s q✝)
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
rw [trStmts₁_run] at h
case refine'_1.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : (l = go k✝ s q✝ ∨ l = ret q✝) ∨ l ∈ trStmts₁ q✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
case refine'_1.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : l ∈ {go k✝ s q✝, ret q✝} ∪ trStmts₁ q✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
simp only [TM2to1.trStmts₁_run, Finset.mem_union, Finset.mem_insert, Finset.mem_singleton]
  at h
case refine'_1.intro.inl.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ s q✝))

case refine'_1.intro.inl.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M (ret q✝))

case refine'_1.intro.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : l ∈ trStmts₁ q✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
case refine'_1.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : (l = go k✝ s q✝ ∨ l = ret q✝) ∨ l ∈ trStmts₁ q✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
rcases h with (⟨rfl | rfl⟩ | h)
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ Γ' → σ → go k✝ s q✝ ∈ trSupp M S
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (stRun s q✝))
simp only [trNormal_run, TM1.SupportsStmt]
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : Γ'
v✝ : σ
⊢ go k✝ s q✝ ∈ trSupp M S
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ Γ' → σ → go k✝ s q✝ ∈ trSupp M S
intros
no goals
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : Γ'
v✝ : σ
⊢ go k✝ s q✝ ∈ trSupp M S
exact hgo
case refine'_1.intro.inl.inl.push
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : σ → Γ k✝
sub : ∀ (x : Λ'), (x = go k✝ (StAct.push a✝) q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ (StAct.push a✝) q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ (StAct.push a✝) q✝))

case refine'_1.intro.inl.inl.peek
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : σ → Option (Γ k✝) → σ
sub : ∀ (x : Λ'), (x = go k✝ (StAct.peek a✝) q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ (StAct.peek a✝) q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ (StAct.peek a✝) q✝))

case refine'_1.intro.inl.inl.pop
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : σ → Option (Γ k✝) → σ
sub : ∀ (x : Λ'), (x = go k✝ (StAct.pop a✝) q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ (StAct.pop a✝) q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ (StAct.pop a✝) q✝))
case refine'_1.intro.inl.inl
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ s q✝))
cases s
no goals
case refine'_1.intro.inl.inl.push
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : σ → Γ k✝
sub : ∀ (x : Λ'), (x = go k✝ (StAct.push a✝) q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ (StAct.push a✝) q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ (StAct.push a✝) q✝))
exact ⟨fun _ _ ↦ hret, fun _ _ ↦ hgo⟩
no goals
case refine'_1.intro.inl.inl.peek
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : σ → Option (Γ k✝) → σ
sub : ∀ (x : Λ'), (x = go k✝ (StAct.peek a✝) q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ (StAct.peek a✝) q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ (StAct.peek a✝) q✝))
exact ⟨fun _ _ ↦ hret, fun _ _ ↦ hgo⟩
no goals
case refine'_1.intro.inl.inl.pop
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
a✝ : σ → Option (Γ k✝) → σ
sub : ∀ (x : Λ'), (x = go k✝ (StAct.pop a✝) q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ (StAct.pop a✝) q✝ ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (tr M (go k✝ (StAct.pop a✝) q✝))
exact ⟨⟨fun _ _ ↦ hret, fun _ _ ↦ hret⟩, fun _ _ ↦ hgo⟩
case refine'_1.intro.inl.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ match
    match ret q✝ with
    | normal q => trNormal (M q)
    | go k s q =>
      branch (fun a x => Option.isNone (Prod.snd a k)) (trStAct (goto fun x x => ret q) s)
        (move Dir.right (goto fun x x => go k s q))
    | ret q => branch (fun a x => a.fst) (trNormal q) (move Dir.left (goto fun x x => ret q)) with
  | move a q => TM1.SupportsStmt (trSupp M S) q
  | write a q => TM1.SupportsStmt (trSupp M S) q
  | load a q => TM1.SupportsStmt (trSupp M S) q
  | branch a q₁ q₂ => TM1.SupportsStmt (trSupp M S) q₁ ∧ TM1.SupportsStmt (trSupp M S) q₂
  | goto l => ∀ (a : Γ') (v : σ), l a v ∈ trSupp M S
  | halt => True
case refine'_1.intro.inl.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (tr M (ret q✝))
unfold TM1.SupportsStmt TM2to1.tr
no goals
case refine'_1.intro.inl.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ match
    match ret q✝ with
    | normal q => trNormal (M q)
    | go k s q =>
      branch (fun a x => Option.isNone (Prod.snd a k)) (trStAct (goto fun x x => ret q) s)
        (move Dir.right (goto fun x x => go k s q))
    | ret q => branch (fun a x => a.fst) (trNormal q) (move Dir.left (goto fun x x => ret q)) with
  | move a q => TM1.SupportsStmt (trSupp M S) q
  | write a q => TM1.SupportsStmt (trSupp M S) q
  | load a q => TM1.SupportsStmt (trSupp M S) q
  | branch a q₁ q₂ => TM1.SupportsStmt (trSupp M S) q₁ ∧ TM1.SupportsStmt (trSupp M S) q₂
  | goto l => ∀ (a : Γ') (v : σ), l a v ∈ trSupp M S
  | halt => True
exact ⟨IH₁, fun _ _ ↦ hret⟩
no goals
case refine'_1.intro.inr
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
k✝ : K
s : StAct k✝
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S q✝
sub : ∀ (x : Λ'), (x = go k✝ s q✝ ∨ x = ret q✝) ∨ x ∈ trStmts₁ q✝ → x ∈ trSupp M S
hgo : go k✝ s q✝ ∈ trSupp M S
hret : ret q✝ ∈ trSupp M S
IH₁ : TM1.SupportsStmt (trSupp M S) (trNormal q✝)
IH₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : l ∈ trStmts₁ q✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
exact IH₂ _ h
case refine'_2
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
a✝ : σ → σ
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.load a✝ q✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.load a✝ q✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a✝ q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.load a✝ q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_2
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (a : σ → σ) (q : Stmt₂),
    (TM2.SupportsStmt S q →
        (∀ (x : Λ'), x ∈ trStmts₁ q → x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q) ∧
            ∀ (l' : Λ'), l' ∈ trStmts₁ q → TM1.SupportsStmt (trSupp M S) (tr M l')) →
      TM2.SupportsStmt S (TM2.Stmt.load a q) →
        (∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.load a q) → x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a q)) ∧
            ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.load a q) → TM1.SupportsStmt (trSupp M S) (tr M l')
intro _ _ IH ss' sub
case refine'_2
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
a✝ : σ → σ
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.load a✝ q✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a✝ q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_2
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
a✝ : σ → σ
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.load a✝ q✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.load a✝ q✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a✝ q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.load a✝ q✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
unfold TM2to1.trStmts₁ at ss' sub⊢
no goals
case refine'_2
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
a✝ : σ → σ
q✝ : Stmt₂
IH :
  TM2.SupportsStmt S q✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.load a✝ q✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q✝ → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.load a✝ q✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ q✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
exact IH ss' sub
case refine'_3
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_3
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (p : σ → Bool) (q₁ q₂ : Stmt₂),
    (TM2.SupportsStmt S q₁ →
        (∀ (x : Λ'), x ∈ trStmts₁ q₁ → x ∈ trSupp M S) →
          TM1.SupportsStmt (trSupp M S) (trNormal q₁) ∧
            ∀ (l' : Λ'), l' ∈ trStmts₁ q₁ → TM1.SupportsStmt (trSupp M S) (tr M l')) →
      (TM2.SupportsStmt S q₂ →
          (∀ (x : Λ'), x ∈ trStmts₁ q₂ → x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal q₂) ∧
              ∀ (l' : Λ'), l' ∈ trStmts₁ q₂ → TM1.SupportsStmt (trSupp M S) (tr M l')) →
        TM2.SupportsStmt S (TM2.Stmt.branch p q₁ q₂) →
          (∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.branch p q₁ q₂) → x ∈ trSupp M S) →
            TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p q₁ q₂)) ∧
              ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.branch p q₁ q₂) → TM1.SupportsStmt (trSupp M S) (tr M l')
intro _ _ _ IH₁ IH₂ ss' sub
case refine'_3
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝ → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_3
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
unfold TM2to1.trStmts₁ at sub
case refine'_3.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝ → x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_3
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝ → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
cases' IH₁ ss'.1 fun x hx ↦ sub x <| Finset.mem_union_left _ hx with IH₁₁ IH₁₂
case refine'_3.intro.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝ → x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₂✝)
IH₂₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_3.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝ → x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
cases' IH₂ ss'.2 fun x hx ↦ sub x <| Finset.mem_union_right _ hx with IH₂₁ IH₂₂
case refine'_3.intro.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝ → x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₂✝)
IH₂₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : l ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝)
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
case refine'_3.intro.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝ → x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₂✝)
IH₂₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.branch p✝ q₁✝ q₂✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
refine' ⟨⟨IH₁₁, IH₂₁⟩, fun l h ↦ _⟩
case refine'_3.intro.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝ → x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₂✝)
IH₂₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : l ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
case refine'_3.intro.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝ → x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₂✝)
IH₂₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : l ∈ trStmts₁ (TM2.Stmt.branch p✝ q₁✝ q₂✝)
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
rw [trStmts₁] at h
no goals
case refine'_3.intro.intro
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
p✝ : σ → Bool
q₁✝ q₂✝ : Stmt₂
IH₁ :
  TM2.SupportsStmt S q₁✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₁✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₁✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂ :
  TM2.SupportsStmt S q₂✝ →
    (∀ (x : Λ'), x ∈ trStmts₁ q₂✝ → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal q₂✝) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
ss' : TM2.SupportsStmt S (TM2.Stmt.branch p✝ q₁✝ q₂✝)
sub : ∀ (x : Λ'), x ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝ → x ∈ trSupp M S
IH₁₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₁✝)
IH₁₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₁✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
IH₂₁ : TM1.SupportsStmt (trSupp M S) (trNormal q₂✝)
IH₂₂ : ∀ (l' : Λ'), l' ∈ trStmts₁ q₂✝ → TM1.SupportsStmt (trSupp M S) (tr M l')
l : Λ'
h : l ∈ trStmts₁ q₁✝ ∪ trStmts₁ q₂✝
⊢ TM1.SupportsStmt (trSupp M S) (tr M l)
rcases Finset.mem_union.1 h with (h | h) <;> [exact IH₁₂ _ h; exact IH₂₂ _ h]
case refine'_4
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.goto l✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.goto l✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_4
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ ∀ (l : σ → Λ),
    TM2.SupportsStmt S (TM2.Stmt.goto l) →
      (∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.goto l) → x ∈ trSupp M S) →
        TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l)) ∧
          ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.goto l) → TM1.SupportsStmt (trSupp M S) (tr M l')
intro _ ss' _
case refine'_4
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.goto l✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝)) ∧
    ∀ (l' : Λ'), False → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_4
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.goto l✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝)) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ (TM2.Stmt.goto l✝) → TM1.SupportsStmt (trSupp M S) (tr M l')
simp only [trStmts₁, Finset.not_mem_empty]
case refine'_4
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.goto l✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝))
case refine'_4
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.goto l✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝)) ∧
    ∀ (l' : Λ'), False → TM1.SupportsStmt (trSupp M S) (tr M l')
refine' ⟨_, fun _ ↦ False.elim⟩
no goals
case refine'_4
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
l✝ : σ → Λ
ss' : TM2.SupportsStmt S (TM2.Stmt.goto l✝)
x✝ : ∀ (x : Λ'), x ∈ trStmts₁ (TM2.Stmt.goto l✝) → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal (TM2.Stmt.goto l✝))
exact fun _ v ↦ Finset.mem_biUnion.2 ⟨_, ss' v, Finset.mem_insert_self _ _⟩
case refine'_5
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
x✝¹ : TM2.SupportsStmt S TM2.Stmt.halt
x✝ : ∀ (x : Λ'), x ∈ trStmts₁ TM2.Stmt.halt → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ TM2.Stmt.halt → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_5
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
⊢ TM2.SupportsStmt S TM2.Stmt.halt →
    (∀ (x : Λ'), x ∈ trStmts₁ TM2.Stmt.halt → x ∈ trSupp M S) →
      TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
        ∀ (l' : Λ'), l' ∈ trStmts₁ TM2.Stmt.halt → TM1.SupportsStmt (trSupp M S) (tr M l')
intro _ _
case refine'_5
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
x✝¹ : TM2.SupportsStmt S TM2.Stmt.halt
x✝ : ∀ (x : Λ'), x ∈ trStmts₁ TM2.Stmt.halt → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧ ∀ (l' : Λ'), False → TM1.SupportsStmt (trSupp M S) (tr M l')
case refine'_5
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
x✝¹ : TM2.SupportsStmt S TM2.Stmt.halt
x✝ : ∀ (x : Λ'), x ∈ trStmts₁ TM2.Stmt.halt → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧
    ∀ (l' : Λ'), l' ∈ trStmts₁ TM2.Stmt.halt → TM1.SupportsStmt (trSupp M S) (tr M l')
simp only [trStmts₁, Finset.not_mem_empty]
no goals
case refine'_5
K : Type u_2
inst✝² : DecidableEq K
Γ : K → Type u_3
Λ : Type u_1
inst✝¹ : Inhabited Λ
σ : Type u_4
inst✝ : Inhabited σ
M : Λ → Stmt₂
S : Finset Λ
ss : TM2.Supports M S
x✝¹ : TM2.SupportsStmt S TM2.Stmt.halt
x✝ : ∀ (x : Λ'), x ∈ trStmts₁ TM2.Stmt.halt → x ∈ trSupp M S
⊢ TM1.SupportsStmt (trSupp M S) (trNormal TM2.Stmt.halt) ∧ ∀ (l' : Λ'), False → TM1.SupportsStmt (trSupp M S) (tr M l')
exact ⟨trivial, fun _ ↦ False.elim⟩