Research proof index

The soundness lemma states that if a term t has type τ in context Γ, then t is semantically valid with respect to Γ and τ

Closing then opening is equivalent to substitution.

Multiple reduction of opening implies multiple reduction of abstraction. -/ theorem redex_abs_cong {M M' : Term Var} (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠ηᶠ M' ^ fvar x) (lc_M : LC M.abs) : M.abs ↠ηᶠ M'.abs := by cases lc_M case abs L hL => have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var rw [open_close x M 0, open_close x M' 0] all_goals...

If a term (λ M) N P_1 ... P_n reduces in a single step to Q, then Q must be one of the following forms: Q = (λ M') N P₁ ... Pₙ where M ⭢βᶠ M' or Q = (λ M) N' P₁ ... Pₙ where N ⭢βᶠ N' or Q = (λ M) N P₁' ... Pₙ' where P_i ⭢βᶠ P_i' for some i or Q = (M ^ N) P₁ ... Pₙ

Parallel reduction has the diamond property.

The inclusion (· ⭢ₚ ·) ≤ (· ↠βᶠ ·).