Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine₀
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
c' : Cfg₀
h₁ : c' ∈ step M { q := q, Tape := T }
h₂ : { q := q, Tape := T }.q ∈ S
⊢ c'.q ∈ S
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine₀
S : Set Λ
ss : Supports M S
⊢ ∀ {c c' : Cfg₀}, c' ∈ step M c → c.q ∈ S → c'.q ∈ S
intro ⟨q, T⟩ c' h₁ h₂
case intro.mk.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine₀
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
h₂ : { q := q, Tape := T }.q ∈ S
q' : Λ
a : Stmt₀
h : M q T.head = some (q', a)
h₁ :
  (fun x =>
        match x with
        | (q', a) =>
          { q := q',
            Tape :=
              match a with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
      (q', a) ∈
    step M { q := q, Tape := T }
⊢ ((fun x =>
          match x with
          | (q', a) =>
            { q := q',
              Tape :=
                match a with
                | Stmt.move d => Tape.move d T
                | Stmt.write a => Tape.write a T })
        (q', a)).q ∈
    S
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine₀
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
c' : Cfg₀
h₁ : c' ∈ step M { q := q, Tape := T }
h₂ : { q := q, Tape := T }.q ∈ S
⊢ c'.q ∈ S
rcases Option.map_eq_some'.1 h₁ with ⟨⟨q', a⟩, h, rfl⟩
no goals
case intro.mk.intro
Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : Machine₀
S : Set Λ
ss : Supports M S
q : Λ
T : Tape Γ
h₂ : { q := q, Tape := T }.q ∈ S
q' : Λ
a : Stmt₀
h : M q T.head = some (q', a)
h₁ :
  (fun x =>
        match x with
        | (q', a) =>
          { q := q',
            Tape :=
              match a with
              | Stmt.move d => Tape.move d T
              | Stmt.write a => Tape.write a T })
      (q', a) ∈
    step M { q := q, Tape := T }
⊢ ((fun x =>
          match x with
          | (q', a) =>
            { q := q',
              Tape :=
                match a with
                | Stmt.move d => Tape.move d T
                | Stmt.write a => Tape.write a T })
        (q', a)).q ∈
    S
exact ss.2 h h₂