case app.beta ht₁ _ ht₂ _ => 
  simp at * 
  have ⟨_, h, hc⟩ := inversion_abs ht₁
  injection h with h₁ h₂
  subst h₁ h₂
  exact shift_down_preservation <| subst_preservation hc (shift_up_preservation ht₂)
ctx : Ctx
t : Term
ty : Ty
ctx✝ : Ctx
ty₁✝ ty₂✝ ty✝ : Ty
t✝ : Term
v✝ : Value
ht₁ : ctx✝ ⊢ Term.abs ty✝ t✝ ⋮ Ty.arrow ty₁✝ ty₂✝
a_ih✝¹ : ∀ {t' : Term}, Term.abs ty✝ t✝ ⇒ t' → ctx✝ ⊢ t' ⋮ Ty.arrow ty₁✝ ty₂✝
ht₂ :
  ctx✝ ⊢
    match v✝ with
    | Value.abs ty body => Term.abs ty body ⋮
    ty₁✝
a_ih✝ :
  ∀ {t' : Term},
    (match v✝ with
        | Value.abs ty body => Term.abs ty body) ⇒
        t' →
      ctx✝ ⊢ t' ⋮ ty₁✝
⊢ ctx✝ ⊢
    Term.shift Dir.down 0
      t✝[0 ↦
        Term.shift Dir.up 0
          (match v✝ with
          | Value.abs ty body => Term.abs ty body)] ⋮
    ty₂✝
no goals