case zero'
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.zero' k ⊆ S
⊢ contSupp k ⊆ S

case succ
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
⊢ ∀ (s : Option Γ'),
    Λ'.Supports S
      (ite (s = some Γ'.consₗ) id (Λ'.clear (fun x => decide (x = Γ'.consₗ)) main) (unrev (Λ'.succ (Λ'.ret k))))

case tail
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.tail k ⊆ S
⊢ contSupp k ⊆ S

case cons
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.cons a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ (Cont'.cons₁ a✝ k))

case comp
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.comp a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.comp a✝¹ k))

case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
S : Finset Λ'
c : Code
k : Cont'
Hk : codeSupp c k ⊆ S
⊢ Λ'.Supports S (trNormal c k)
induction c generalizing k <;> simp [Λ'.Supports, head]
case succ
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
⊢ ∀ (s : Option Γ'),
    Λ'.Supports S
      (ite (s = some Γ'.consₗ) id (Λ'.clear (fun x => decide (x = Γ'.consₗ)) main) (unrev (Λ'.succ (Λ'.ret k))))

case tail
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.tail k ⊆ S
⊢ contSupp k ⊆ S

case cons
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.cons a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ (Cont'.cons₁ a✝ k))

case comp
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.comp a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.comp a✝¹ k))

case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case zero'
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.zero' k ⊆ S
⊢ contSupp k ⊆ S

case succ
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
⊢ ∀ (s : Option Γ'),
    Λ'.Supports S
      (ite (s = some Γ'.consₗ) id (Λ'.clear (fun x => decide (x = Γ'.consₗ)) main) (unrev (Λ'.succ (Λ'.ret k))))

case tail
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.tail k ⊆ S
⊢ contSupp k ⊆ S

case cons
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.cons a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ (Cont'.cons₁ a✝ k))

case comp
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.comp a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.comp a✝¹ k))

case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case zero' => exact Finset.union_subset_right Hk
case tail
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.tail k ⊆ S
⊢ contSupp k ⊆ S

case cons
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.cons a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ (Cont'.cons₁ a✝ k))

case comp
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.comp a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.comp a✝¹ k))

case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case succ
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
⊢ ∀ (s : Option Γ'),
    Λ'.Supports S
      (ite (s = some Γ'.consₗ) id (Λ'.clear (fun x => decide (x = Γ'.consₗ)) main) (unrev (Λ'.succ (Λ'.ret k))))

case tail
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.tail k ⊆ S
⊢ contSupp k ⊆ S

case cons
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.cons a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ (Cont'.cons₁ a✝ k))

case comp
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.comp a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.comp a✝¹ k))

case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case succ => intro ; split_ifs <;> exact Finset.union_subset_right Hk
case cons
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.cons a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ (Cont'.cons₁ a✝ k))

case comp
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.comp a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.comp a✝¹ k))

case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case tail
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.tail k ⊆ S
⊢ contSupp k ⊆ S

case cons
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.cons a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ (Cont'.cons₁ a✝ k))

case comp
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.comp a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.comp a✝¹ k))

case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case tail => exact Finset.union_subset_right Hk
case comp
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.comp a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.comp a✝¹ k))

case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case cons
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.cons a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ (Cont'.cons₁ a✝ k))

case comp
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.comp a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.comp a✝¹ k))

case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case cons f fs IHf _ =>
  apply IHf
  rw [codeSupp_cons] at Hk
  exact Finset.union_subset_right Hk
case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case comp
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.comp a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.comp a✝¹ k))

case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case comp f g _ IHg => apply IHg; rw [codeSupp_comp] at Hk; exact Finset.union_subset_right Hk
case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case case
S : Finset Λ'
a✝¹ a✝ : Code
a_ih✝¹ : ∀ {k : Cont'}, codeSupp a✝¹ k ⊆ S → Λ'.Supports S (trNormal a✝¹ k)
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.case a✝¹ a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝¹ k) ∧ Λ'.Supports S (trNormal a✝ k)

case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case
  case f g IHf IHg =>
  simp only [codeSupp_case, Finset.union_subset_iff] at Hk
  exact ⟨IHf Hk.2.1, IHg Hk.2.2⟩
no goals
case fix
S : Finset Λ'
a✝ : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp a✝ k ⊆ S → Λ'.Supports S (trNormal a✝ k)
k : Cont'
Hk : codeSupp (Code.fix a✝) k ⊆ S
⊢ Λ'.Supports S (trNormal a✝ (Cont'.fix a✝ k))
case fix f IHf => apply IHf; rw [codeSupp_fix] at Hk; exact Finset.union_subset_right Hk
no goals
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.zero' k ⊆ S
⊢ contSupp k ⊆ S
exact Finset.union_subset_right Hk
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
s✝ : Option Γ'
⊢ Λ'.Supports S
    (ite (s✝ = some Γ'.consₗ) id (Λ'.clear (fun x => decide (x = Γ'.consₗ)) main) (unrev (Λ'.succ (Λ'.ret k))))
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
⊢ ∀ (s : Option Γ'),
    Λ'.Supports S
      (ite (s = some Γ'.consₗ) id (Λ'.clear (fun x => decide (x = Γ'.consₗ)) main) (unrev (Λ'.succ (Λ'.ret k))))
intro
no goals
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.succ k ⊆ S
s✝ : Option Γ'
⊢ Λ'.Supports S
    (ite (s✝ = some Γ'.consₗ) id (Λ'.clear (fun x => decide (x = Γ'.consₗ)) main) (unrev (Λ'.succ (Λ'.ret k))))
split_ifs <;> exact Finset.union_subset_right Hk
no goals
S : Finset Λ'
k : Cont'
Hk : codeSupp Code.tail k ⊆ S
⊢ contSupp k ⊆ S
exact Finset.union_subset_right Hk
case Hk
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (Code.cons f fs) k ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (Code.cons f fs) k ⊆ S
⊢ Λ'.Supports S (trNormal f (Cont'.cons₁ fs k))
apply IHf
case Hk
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : trStmts₁ (trNormal (Code.cons f fs) k) ∪ codeSupp f (Cont'.cons₁ fs k) ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S
case Hk
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : codeSupp (Code.cons f fs) k ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S
rw [codeSupp_cons] at Hk
no goals
case Hk
S : Finset Λ'
f fs : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
a_ih✝ : ∀ {k : Cont'}, codeSupp fs k ⊆ S → Λ'.Supports S (trNormal fs k)
k : Cont'
Hk : trStmts₁ (trNormal (Code.cons f fs) k) ∪ codeSupp f (Cont'.cons₁ fs k) ⊆ S
⊢ codeSupp f (Cont'.cons₁ fs k) ⊆ S
exact Finset.union_subset_right Hk
case Hk
S : Finset Λ'
f g : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : codeSupp (Code.comp f g) k ⊆ S
⊢ codeSupp g (Cont'.comp f k) ⊆ S
S : Finset Λ'
f g : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : codeSupp (Code.comp f g) k ⊆ S
⊢ Λ'.Supports S (trNormal g (Cont'.comp f k))
apply IHg
case Hk
S : Finset Λ'
f g : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : trStmts₁ (trNormal (Code.comp f g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
⊢ codeSupp g (Cont'.comp f k) ⊆ S
case Hk
S : Finset Λ'
f g : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : codeSupp (Code.comp f g) k ⊆ S
⊢ codeSupp g (Cont'.comp f k) ⊆ S
rw [codeSupp_comp] at Hk
no goals
case Hk
S : Finset Λ'
f g : Code
a_ih✝ : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : trStmts₁ (trNormal (Code.comp f g) k) ∪ codeSupp g (Cont'.comp f k) ⊆ S
⊢ codeSupp g (Cont'.comp f k) ⊆ S
exact Finset.union_subset_right Hk
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : trStmts₁ (trNormal (Code.case f g) k) ⊆ S ∧ codeSupp f k ⊆ S ∧ codeSupp g k ⊆ S
⊢ Λ'.Supports S (trNormal f k) ∧ Λ'.Supports S (trNormal g k)
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : codeSupp (Code.case f g) k ⊆ S
⊢ Λ'.Supports S (trNormal f k) ∧ Λ'.Supports S (trNormal g k)
simp only [codeSupp_case, Finset.union_subset_iff] at Hk
no goals
S : Finset Λ'
f g : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
IHg : ∀ {k : Cont'}, codeSupp g k ⊆ S → Λ'.Supports S (trNormal g k)
k : Cont'
Hk : trStmts₁ (trNormal (Code.case f g) k) ⊆ S ∧ codeSupp f k ⊆ S ∧ codeSupp g k ⊆ S
⊢ Λ'.Supports S (trNormal f k) ∧ Λ'.Supports S (trNormal g k)
exact ⟨IHf Hk.2.1, IHg Hk.2.2⟩
case Hk
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
k : Cont'
Hk : codeSupp (Code.fix f) k ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
k : Cont'
Hk : codeSupp (Code.fix f) k ⊆ S
⊢ Λ'.Supports S (trNormal f (Cont'.fix f k))
apply IHf
case Hk
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
k : Cont'
Hk : trStmts₁ (trNormal (Code.fix f) k) ∪ codeSupp f (Cont'.fix f k) ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S
case Hk
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
k : Cont'
Hk : codeSupp (Code.fix f) k ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S
rw [codeSupp_fix] at Hk
no goals
case Hk
S : Finset Λ'
f : Code
IHf : ∀ {k : Cont'}, codeSupp f k ⊆ S → Λ'.Supports S (trNormal f k)
k : Cont'
Hk : trStmts₁ (trNormal (Code.fix f) k) ∪ codeSupp f (Cont'.fix f k) ⊆ S
⊢ codeSupp f (Cont'.fix f k) ⊆ S
exact Finset.union_subset_right Hk