Progress

theorem progress {t : Term Var} {τ : Ty Base} (ht : [] ⊢ t ∶ τ) : t.Value ∨ ∃ t', t ⭢βᶠ t' := by  generalize eq : [] = Γ at ht  induction ht  case var => simp_all  case abs xs mem ih =>    left    constructor    apply Term.LC.abs xs    intros _ mem'    exact (mem _ mem').lc  case app Γ M σ τ N der_l der_r ih_l ih_r =>    simp only [eq, forall_const] at *    right    cases ih_l with    -- if the lhs is a value, beta reduce the application    | inl val => cases val with | abs M _ => use M ^ N, by grind    -- otherwise, propagate the step to the lhs of the application    | inr step =>      obtain ⟨M', _⟩ := step      use M'.app N      grind