case nil
q : Λ'
s✝ : Option Γ'
a✝ c d✝ : List Γ'
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.copy q), var := s, stk := elim a [] c d }
    { l := some q, var := none, stk := elim (List.reverseAux [] a) [] c (List.reverseAux [] d) }

case cons
q : Λ'
s✝ : Option Γ'
a✝ c d✝ : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some (Λ'.copy q), var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (List.reverseAux b a) [] c (List.reverseAux b d) }
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.copy q), var := s, stk := elim a (x :: b) c d }
    { l := some q, var := none, stk := elim (List.reverseAux (x :: b) a) [] c (List.reverseAux (x :: b) d) }
q : Λ'
s : Option Γ'
a b c d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.copy q), var := s, stk := elim a b c d }
    { l := some q, var := none, stk := elim (List.reverseAux b a) [] c (List.reverseAux b d) }
induction' b with x b IH generalizing a d s
case cons
q : Λ'
s✝ : Option Γ'
a✝ c d✝ : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some (Λ'.copy q), var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (List.reverseAux b a) [] c (List.reverseAux b d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen (fun a b => b ∈ TM2.step tr a) (TM2.stepAux (tr (Λ'.copy q)) s (elim a (x :: b) c d))
    { l := some q, var := none, stk := elim (List.reverseAux (x :: b) a) [] c (List.reverseAux (x :: b) d) }
case cons
q : Λ'
s✝ : Option Γ'
a✝ c d✝ : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some (Λ'.copy q), var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (List.reverseAux b a) [] c (List.reverseAux b d) }
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.copy q), var := s, stk := elim a (x :: b) c d }
    { l := some q, var := none, stk := elim (List.reverseAux (x :: b) a) [] c (List.reverseAux (x :: b) d) }
refine' TransGen.head rfl _
case cons
q : Λ'
s✝ : Option Γ'
a✝ c d✝ : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some (Λ'.copy q), var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (List.reverseAux b a) [] c (List.reverseAux b d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen
    (fun a b =>
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (Λ'.copy q), var := some x, stk := elim (Option.iget (some x) :: a) b c (Option.iget (some x) :: d) }
    { l := some q, var := none, stk := elim (List.reverseAux b (x :: a)) [] c (List.reverseAux b (x :: d)) }
case cons
q : Λ'
s✝ : Option Γ'
a✝ c d✝ : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some (Λ'.copy q), var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (List.reverseAux b a) [] c (List.reverseAux b d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen (fun a b => b ∈ TM2.step tr a) (TM2.stepAux (tr (Λ'.copy q)) s (elim a (x :: b) c d))
    { l := some q, var := none, stk := elim (List.reverseAux (x :: b) a) [] c (List.reverseAux (x :: b) d) }
simp
no goals
case cons
q : Λ'
s✝ : Option Γ'
a✝ c d✝ : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step tr) { l := some (Λ'.copy q), var := s, stk := elim a b c d }
      { l := some q, var := none, stk := elim (List.reverseAux b a) [] c (List.reverseAux b d) }
s : Option Γ'
a d : List Γ'
⊢ TransGen
    (fun a b =>
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (Λ'.copy q), var := some x, stk := elim (Option.iget (some x) :: a) b c (Option.iget (some x) :: d) }
    { l := some q, var := none, stk := elim (List.reverseAux b (x :: a)) [] c (List.reverseAux b (x :: d)) }
exact IH _ _ _
case nil
q : Λ'
s✝ : Option Γ'
a✝ c d✝ : List Γ'
s : Option Γ'
a d : List Γ'
⊢ { l := some q, var := none, stk := elim (List.reverseAux [] a) [] c (List.reverseAux [] d) } ∈
    TM2.step tr { l := some (Λ'.copy q), var := s, stk := elim a [] c d }
case nil
q : Λ'
s✝ : Option Γ'
a✝ c d✝ : List Γ'
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.copy q), var := s, stk := elim a [] c d }
    { l := some q, var := none, stk := elim (List.reverseAux [] a) [] c (List.reverseAux [] d) }
refine' TransGen.single _
no goals
case nil
q : Λ'
s✝ : Option Γ'
a✝ c d✝ : List Γ'
s : Option Γ'
a d : List Γ'
⊢ { l := some q, var := none, stk := elim (List.reverseAux [] a) [] c (List.reverseAux [] d) } ∈
    TM2.step tr { l := some (Λ'.copy q), var := s, stk := elim a [] c d }
simp