inductive SimplyTyped.Typ : Type

• var: Name → SimplyTyped.Typ
• arrow: SimplyTyped.Typ → SimplyTyped.Typ → SimplyTyped.Typ

instance SimplyTyped.instReprTyp : Repr SimplyTyped.Typ

Equations

• SimplyTyped.instReprTyp = { reprPrec := SimplyTyped.reprTyp✝ }

instance SimplyTyped.instDecidableEqTyp : DecidableEq SimplyTyped.Typ

Equations

• SimplyTyped.instDecidableEqTyp = SimplyTyped.decEqTyp✝

def SimplyTyped.Typ.toString : SimplyTyped.Typ → String

Equations

• (SimplyTyped.Typ.var a).toString = a
• (a ⇒ a_1).toString = toString "" ++ toString a.toString ++ toString " → " ++ toString a_1.toString ++ toString ""

instance SimplyTyped.Typ.instToString : ToString SimplyTyped.Typ

Equations

• SimplyTyped.Typ.instToString = { toString := SimplyTyped.Typ.toString }

instance SimplyTyped.Typ.instCoeName : Coe Name SimplyTyped.Typ

Equations

• SimplyTyped.Typ.instCoeName = { coe := SimplyTyped.Typ.var }

def SimplyTyped.Typ.«term_⇒_» : Lean.TrailingParserDescr

Equations

• SimplyTyped.Typ.«term_⇒_» = Lean.ParserDescr.trailingNode `SimplyTyped.Typ.term_⇒_ 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇒ ") (Lean.ParserDescr.cat `term 20))

inductive SimplyTyped.Term : Type

• var: Name → SimplyTyped.Term
• app: SimplyTyped.Term → SimplyTyped.Term → SimplyTyped.Term
• abs: Name → SimplyTyped.Typ → SimplyTyped.Term → SimplyTyped.Term

instance SimplyTyped.instReprTerm : Repr SimplyTyped.Term

Equations

• SimplyTyped.instReprTerm = { reprPrec := SimplyTyped.reprTerm✝ }

instance SimplyTyped.instDecidableEqTerm : DecidableEq SimplyTyped.Term

Equations

• SimplyTyped.instDecidableEqTerm = SimplyTyped.decEqTerm✝

def SimplyTyped.Term.toString : SimplyTyped.Term → String

Equations

• (SimplyTyped.Term.var a).toString = a
• (a ∙ a_1).toString = toString "(" ++ toString a.toString ++ toString " " ++ toString a_1.toString ++ toString ")"
• (SimplyTyped.Term.abs a a_1 a_2).toString = toString "(λ" ++ toString a ++ toString " : " ++ toString a_1 ++ toString ". " ++ toString a_2.toString ++ toString ")"

instance SimplyTyped.Term.instToString : ToString SimplyTyped.Term

Equations

• SimplyTyped.Term.instToString = { toString := SimplyTyped.Term.toString }

instance SimplyTyped.Term.instCoeName : Coe Name SimplyTyped.Term

Equations

• SimplyTyped.Term.instCoeName = { coe := SimplyTyped.Term.var }

def SimplyTyped.Term.«term_∙_» : Lean.TrailingParserDescr

Equations

• SimplyTyped.Term.«term_∙_» = Lean.ParserDescr.trailingNode `SimplyTyped.Term.term_∙_ 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∙ ") (Lean.ParserDescr.cat `term 101))

def SimplyTyped.Term.Sub (L : SimplyTyped.Term) : Multiset SimplyTyped.Term

Equations

• (SimplyTyped.Term.var a).Sub = {SimplyTyped.Term.var a}
• (a ∙ a_1).Sub = a ∙ a_1 ::ₘ (a.Sub + a_1.Sub)
• (SimplyTyped.Term.abs a a_1 a_2).Sub = SimplyTyped.Term.abs a a_1 a_2 ::ₘ a_2.Sub

def SimplyTyped.Term.Subterm (L : SimplyTyped.Term) (M : SimplyTyped.Term) : Prop

Equations

• L.Subterm M = (L ∈ M.Sub)

instance SimplyTyped.Term.instHasSubset : HasSubset SimplyTyped.Term

Equations

• SimplyTyped.Term.instHasSubset = { Subset := SimplyTyped.Term.Subterm }

instance SimplyTyped.Term.instDecidableSubterm {M : SimplyTyped.Term} {N : SimplyTyped.Term} : Decidable (M.Subterm N)

Equations

• SimplyTyped.Term.instDecidableSubterm = inferInstanceAs (Decidable (M ∈ N.Sub))

instance SimplyTyped.Term.instDecidableSubset {M : SimplyTyped.Term} {N : SimplyTyped.Term} : Decidable (M ⊆ N)

Equations

• SimplyTyped.Term.instDecidableSubset = inferInstanceAs (Decidable (M ∈ N.Sub))

def SimplyTyped.Term.FV : SimplyTyped.Term → Finset Name

Equations

• (SimplyTyped.Term.var a).FV = {a}
• (a ∙ a_1).FV = a.FV ∪ a_1.FV
• (SimplyTyped.Term.abs a a_1 a_2).FV = a_2.FV \ {a}

@[reducible, inline]

abbrev SimplyTyped.Declaration : Type

Equations

• SimplyTyped.Declaration = (Name × SimplyTyped.Typ)

@[reducible, inline]

abbrev SimplyTyped.Context : Type

Equations

• SimplyTyped.Context = Finset SimplyTyped.Declaration

inductive SimplyTyped.Judgement : SimplyTyped.Context → SimplyTyped.Term → SimplyTyped.Typ → Prop

• var: ∀ {Γ : SimplyTyped.Context} {x : Name} {σ : SimplyTyped.Typ}, (x, σ) ∈ Γ → Γ ⊢ SimplyTyped.Term.var x : σ
• app: ∀ {Γ : SimplyTyped.Context} {M N : SimplyTyped.Term} {σ τ : SimplyTyped.Typ}, (Γ ⊢ M : σ ⇒ τ) → (Γ ⊢ N : σ) → Γ ⊢ M ∙ N : τ
• abs: ∀ {Γ : SimplyTyped.Context} {x : Name} {M : SimplyTyped.Term} {σ τ : SimplyTyped.Typ}, (insert (x, σ) Γ ⊢ M : τ) → Γ ⊢ SimplyTyped.Term.abs x σ M : σ ⇒ τ

def SimplyTyped.«term_⊢_:_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def SimplyTyped.Statement (M : SimplyTyped.Term) (σ : SimplyTyped.Typ) : Prop

Equations

• (⊢ M : σ) = ∃ (Γ : SimplyTyped.Context), Γ ⊢ M : σ

def SimplyTyped.«term⊢_:_» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def SimplyTyped.Typeable (M : SimplyTyped.Term) : Prop

Equations

• SimplyTyped.Typeable M = ∃ (σ : SimplyTyped.Typ), ⊢ M : σ

def SimplyTyped.Legal (M : SimplyTyped.Term) : Prop

Equations

• SimplyTyped.Legal M = ∃ (Γ : SimplyTyped.Context) (ρ : SimplyTyped.Typ), Γ ⊢ M : ρ

def SimplyTyped.dom (Γ : SimplyTyped.Context) : Finset Name

Equations

• SimplyTyped.dom Γ = Finset.image Prod.fst Γ

def SimplyTyped.Subcontext (Γ : SimplyTyped.Context) (Δ : SimplyTyped.Context) : Prop

Equations

• SimplyTyped.Subcontext Γ Δ = (Δ ⊆ Γ)

def SimplyTyped.Permutation (Γ : SimplyTyped.Context) (Δ : SimplyTyped.Context) : Prop

Equations

• SimplyTyped.Permutation Γ Δ = (SimplyTyped.dom Δ = SimplyTyped.dom Γ)

def SimplyTyped.projection (Γ : SimplyTyped.Context) (Φ : Finset Name) : SimplyTyped.Context

Equations

• Γ ↾ Φ = Finset.filter (fun (x : SimplyTyped.Declaration) => x.1 ∈ SimplyTyped.dom Γ ∩ Φ) Γ

def SimplyTyped.«term_↾_» : Lean.TrailingParserDescr

Equations

• SimplyTyped.«term_↾_» = Lean.ParserDescr.trailingNode `SimplyTyped.term_↾_ 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↾ ") (Lean.ParserDescr.cat `term 61))

theorem SimplyTyped.dom_insert_eq_insert_dom {Γ : SimplyTyped.Context} {x : Name} {σ : SimplyTyped.Typ} : SimplyTyped.dom (insert (x, σ) Γ) = insert x (SimplyTyped.dom Γ)

theorem SimplyTyped.Finset.diff_subset_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} : s \ t ⊆ u ↔ s ⊆ t ∪ u

theorem SimplyTyped.context_free_variables {Γ : SimplyTyped.Context} {L : SimplyTyped.Term} {σ : SimplyTyped.Typ} (J : Γ ⊢ L : σ) : L.FV ⊆ SimplyTyped.dom Γ

@[simp]

theorem SimplyTyped.thinning {Γ : SimplyTyped.Context} {Δ : SimplyTyped.Context} {M : SimplyTyped.Term} {σ : SimplyTyped.Typ} (h : Γ ⊆ Δ) : (Γ ⊢ M : σ) → Δ ⊢ M : σ

@[simp]

theorem SimplyTyped.condensing {Γ : SimplyTyped.Context} {M : SimplyTyped.Term} {σ : SimplyTyped.Typ} (J : Γ ⊢ M : σ) : (Γ ↾ M.FV) ⊢ M : σ

@[simp]

theorem SimplyTyped.permutation {Γ : SimplyTyped.Context} {Δ : SimplyTyped.Context} {M : SimplyTyped.Term} {σ : SimplyTyped.Typ} (h : SimplyTyped.Permutation Γ Δ) : (Γ ⊢ M : σ) → Δ ⊢ M : σ

@[simp]

theorem SimplyTyped.generation_var {Γ : SimplyTyped.Context} {x : Name} {σ : SimplyTyped.Typ} : (Γ ⊢ SimplyTyped.Term.var x : σ) ↔ (x, σ) ∈ Γ

@[simp]

theorem SimplyTyped.generation_app {Γ : SimplyTyped.Context} {M : SimplyTyped.Term} {N : SimplyTyped.Term} {τ : SimplyTyped.Typ} : (Γ ⊢ M ∙ N : τ) ↔ ∃ (σ : SimplyTyped.Typ), (Γ ⊢ M : σ ⇒ τ) ∧ Γ ⊢ N : σ

@[simp]

theorem SimplyTyped.generation_abs {Γ : SimplyTyped.Context} {x : Name} {M : SimplyTyped.Term} {σ : SimplyTyped.Typ} {ρ : SimplyTyped.Typ} : (Γ ⊢ SimplyTyped.Term.abs x σ M : ρ) ↔ ∃ (τ : SimplyTyped.Typ), (insert (x, σ) Γ ⊢ M : τ) ∧ ρ = (σ ⇒ τ)

theorem SimplyTyped.subterm {M : SimplyTyped.Term} (h : SimplyTyped.Legal M) (N : SimplyTyped.Term) : N ⊆ M → SimplyTyped.Legal N

@[simp]

theorem SimplyTyped.uniqueness_of_types {Γ : SimplyTyped.Context} {M : SimplyTyped.Term} {σ : SimplyTyped.Typ} {τ : SimplyTyped.Typ} (Jσ : Γ ⊢ M : σ) (Jτ : Γ ⊢ M : τ) : σ = τ

def SimplyTyped.WellTyped (M : SimplyTyped.Term) : Prop

Equations

• SimplyTyped.WellTyped M = ∃ (σ : SimplyTyped.Typ), ⊢ M : σ

def SimplyTyped.TypeAssignment (Γ : SimplyTyped.Context) (M : SimplyTyped.Term) : Prop

Equations

• SimplyTyped.TypeAssignment Γ M = ∃ (σ : SimplyTyped.Typ), Γ ⊢ M : σ

def SimplyTyped.TypeChecking (Γ : SimplyTyped.Context) (M : SimplyTyped.Term) (σ : SimplyTyped.Typ) : Prop

Equations

• SimplyTyped.TypeChecking Γ M σ = Γ ⊢ M : σ

def SimplyTyped.TermFinding (Γ : SimplyTyped.Context) (σ : SimplyTyped.Typ) : Prop

Equations

• SimplyTyped.TermFinding Γ σ = ∃ (M : SimplyTyped.Term), Γ ⊢ M : σ

def SimplyTyped.hasDecTypeable (M : SimplyTyped.Term) : Decidable (SimplyTyped.Typeable M)

Equations

• One or more equations did not get rendered due to their size.
• SimplyTyped.hasDecTypeable (SimplyTyped.Term.var a) = id (let σ := SimplyTyped.Typ.var "σ"; let Γ := {(a, σ)}; isTrue ⋯)

def SimplyTyped.hasDecWellTyped (M : SimplyTyped.Term) : Decidable (SimplyTyped.WellTyped M)

Equations

• SimplyTyped.hasDecWellTyped M = SimplyTyped.hasDecTypeable M

def SimplyTyped.hasDecTypeAssignment (Γ : SimplyTyped.Context) (M : SimplyTyped.Term) : Decidable (SimplyTyped.TypeAssignment Γ M)

Equations

• SimplyTyped.hasDecTypeAssignment Γ M = sorryAx (Decidable (SimplyTyped.TypeAssignment Γ M))

def SimplyTyped.hasDecTypeChecking (Γ : SimplyTyped.Context) (M : SimplyTyped.Term) (σ : SimplyTyped.Typ) : Decidable (SimplyTyped.TypeChecking Γ M σ)

Equations

• One or more equations did not get rendered due to their size.
• SimplyTyped.hasDecTypeChecking Γ (SimplyTyped.Term.var a) σ = if h : (a, σ) ∈ Γ then isTrue ⋯ else id (⋯.mpr (isFalse ⋯))

def SimplyTyped.hasDecTermFinding (Γ : SimplyTyped.Context) (σ : SimplyTyped.Typ) : Decidable (SimplyTyped.TermFinding Γ σ)

Equations

• SimplyTyped.hasDecTermFinding Γ σ = sorryAx (Decidable (SimplyTyped.TermFinding Γ σ))

instance SimplyTyped.instDecidableTypeable {M : SimplyTyped.Term} : Decidable (SimplyTyped.Typeable M)

Equations

• SimplyTyped.instDecidableTypeable = SimplyTyped.hasDecTypeable M

instance SimplyTyped.instDecidableWellTyped {M : SimplyTyped.Term} : Decidable (SimplyTyped.WellTyped M)

Equations

• SimplyTyped.instDecidableWellTyped = SimplyTyped.hasDecWellTyped M

instance SimplyTyped.instDecidableTypeAssignment {Γ : SimplyTyped.Context} {M : SimplyTyped.Term} : Decidable (SimplyTyped.TypeAssignment Γ M)

Equations

• SimplyTyped.instDecidableTypeAssignment = SimplyTyped.hasDecTypeAssignment Γ M

instance SimplyTyped.instDecidableTypeChecking {Γ : SimplyTyped.Context} {M : SimplyTyped.Term} {σ : SimplyTyped.Typ} : Decidable (SimplyTyped.TypeChecking Γ M σ)

Equations

• SimplyTyped.instDecidableTypeChecking = SimplyTyped.hasDecTypeChecking Γ M σ

instance SimplyTyped.instDecidableTermFinding {Γ : SimplyTyped.Context} {σ : SimplyTyped.Typ} : Decidable (SimplyTyped.TermFinding Γ σ)

Equations

• SimplyTyped.instDecidableTermFinding = SimplyTyped.hasDecTermFinding Γ σ

def SimplyTyped.subst (M : SimplyTyped.Term) (x : Name) (N : SimplyTyped.Term) : SimplyTyped.Term

Equations

• SimplyTyped.subst (SimplyTyped.Term.var a) x N = if x = a then N else SimplyTyped.Term.var a
• SimplyTyped.subst (a ∙ a_1) x N = SimplyTyped.subst a x N ∙ SimplyTyped.subst a_1 x N
• SimplyTyped.subst (SimplyTyped.Term.abs a a_1 a_2) x N = if x = a ∨ a ∈ N.FV then SimplyTyped.Term.abs a a_1 a_2 else SimplyTyped.Term.abs a a_1 (SimplyTyped.subst a_2 x N)

def SimplyTyped.«term_[_:=_,_]» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem SimplyTyped.substitution {Γ : SimplyTyped.Context} {Δ : SimplyTyped.Context} {M : SimplyTyped.Term} {N : SimplyTyped.Term} {x : Name} {σ : SimplyTyped.Typ} {τ : SimplyTyped.Typ} (hM : insert (x, σ) (Γ ∪ Δ) ⊢ M : τ) (hN : Γ ⊢ N : σ) : (Γ ∪ Δ) ⊢ SimplyTyped.subst M x N : τ

def SimplyTyped.reduceβ : SimplyTyped.Term → SimplyTyped.Term

Equations

• SimplyTyped.reduceβ (SimplyTyped.Term.abs x_1 type M ∙ N) = SimplyTyped.subst M x_1 N
• SimplyTyped.reduceβ (SimplyTyped.Term.var x_1) = SimplyTyped.Term.var x_1
• SimplyTyped.reduceβ (M ∙ N) = SimplyTyped.reduceβ M ∙ SimplyTyped.reduceβ N
• SimplyTyped.reduceβ (SimplyTyped.Term.abs x_1 σ M) = SimplyTyped.Term.abs x_1 σ (SimplyTyped.reduceβ M)

inductive SimplyTyped.Beta : SimplyTyped.Term → SimplyTyped.Term → Prop

• redex: ∀ {x : Name} {σ : SimplyTyped.Typ} (M N : SimplyTyped.Term), SimplyTyped.Term.abs x σ M ∙ N →β SimplyTyped.subst M x N
• compatAppLeft: ∀ {L M N : SimplyTyped.Term}, M →β N → M ∙ L →β N ∙ L
• compatAppRight: ∀ {L M N : SimplyTyped.Term}, M →β N → L ∙ M →β L ∙ N
• compatAbs: ∀ {x : Name} {σ : SimplyTyped.Typ} {M N : SimplyTyped.Term}, M →β N → SimplyTyped.Term.abs x σ M →β SimplyTyped.Term.abs x σ N

def SimplyTyped.«term_→β_» : Lean.TrailingParserDescr

Equations

• SimplyTyped.«term_→β_» = Lean.ParserDescr.trailingNode `SimplyTyped.term_→β_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →β ") (Lean.ParserDescr.cat `term 51))

def SimplyTyped.«term_←β_» : Lean.TrailingParserDescr

Equations

• SimplyTyped.«term_←β_» = Lean.ParserDescr.trailingNode `SimplyTyped.term_←β_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ←β ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem SimplyTyped.beta_redex {x : Name} {σ : SimplyTyped.Typ} {M : SimplyTyped.Term} {N : SimplyTyped.Term} : SimplyTyped.Term.abs x σ M ∙ N →β SimplyTyped.subst M x N

@[simp]

theorem SimplyTyped.beta_compat_app_left {L : SimplyTyped.Term} {M : SimplyTyped.Term} {N : SimplyTyped.Term} (h : M →β N) : M ∙ L →β N ∙ L

@[simp]

theorem SimplyTyped.beta_compat_app_right {L : SimplyTyped.Term} {M : SimplyTyped.Term} {N : SimplyTyped.Term} (h : M →β N) : L ∙ M →β L ∙ N

@[simp]

theorem SimplyTyped.beta_compat_abs {x : Name} {σ : SimplyTyped.Typ} {M : SimplyTyped.Term} {N : SimplyTyped.Term} (h : M →β N) : SimplyTyped.Term.abs x σ M →β SimplyTyped.Term.abs x σ N

@[reducible, inline]

abbrev SimplyTyped.BetaChain (a : SimplyTyped.Term) : SimplyTyped.Term → Prop

Equations

• SimplyTyped.BetaChain = Relation.ReflTransGen SimplyTyped.Beta

def SimplyTyped.«term_↠β_» : Lean.TrailingParserDescr

Equations

• SimplyTyped.«term_↠β_» = Lean.ParserDescr.trailingNode `SimplyTyped.term_↠β_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↠β ") (Lean.ParserDescr.cat `term 51))

def SimplyTyped.«term_↞β_» : Lean.TrailingParserDescr

Equations

• SimplyTyped.«term_↞β_» = Lean.ParserDescr.trailingNode `SimplyTyped.term_↞β_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↞β ") (Lean.ParserDescr.cat `term 51))

theorem SimplyTyped.BetaChain.extension {M : SimplyTyped.Term} {N : SimplyTyped.Term} : M →β N → M ↠β N

instance SimplyTyped.instCoeBetaBetaChain {M : SimplyTyped.Term} {N : SimplyTyped.Term} : Coe (M →β N) (M ↠β N)

Equations

• SimplyTyped.instCoeBetaBetaChain = { coe := ⋯ }

inductive SimplyTyped.BetaEq : SimplyTyped.Term → SimplyTyped.Term → Prop

• beta: ∀ {M N : SimplyTyped.Term}, M →β N → M =β N
• betaInv: ∀ {M N : SimplyTyped.Term}, N →β M → M =β N
• refl: ∀ (M : SimplyTyped.Term), M =β M
• symm: ∀ {M N : SimplyTyped.Term}, M =β N → N =β M
• trans: ∀ {L M N : SimplyTyped.Term}, L =β M → M =β N → L =β N

def SimplyTyped.«term_=β_» : Lean.TrailingParserDescr

Equations

• SimplyTyped.«term_=β_» = Lean.ParserDescr.trailingNode `SimplyTyped.term_=β_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =β ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem SimplyTyped.beta_eq_beta {M : SimplyTyped.Term} {N : SimplyTyped.Term} (h : M →β N) : M =β N

@[simp]

theorem SimplyTyped.beta_eq_beta_inv {M : SimplyTyped.Term} {N : SimplyTyped.Term} (h : N →β M) : M =β N

theorem SimplyTyped.beta_eq_refl (M : SimplyTyped.Term) : M =β M

theorem SimplyTyped.beta_eq_symm {M : SimplyTyped.Term} {N : SimplyTyped.Term} (h : M =β N) : N =β M

theorem SimplyTyped.beta_eq_trans {L : SimplyTyped.Term} {M : SimplyTyped.Term} {N : SimplyTyped.Term} (hlm : L =β M) (hmn : M =β N) : L =β N

theorem SimplyTyped.eq_imp_beta_eq {M : SimplyTyped.Term} {N : SimplyTyped.Term} (h : M = N) : M =β N

theorem SimplyTyped.BetaEq.extension {M : SimplyTyped.Term} {N : SimplyTyped.Term} : M ↠β N → M =β N

theorem SimplyTyped.BetaEq.extensionInv {M : SimplyTyped.Term} {N : SimplyTyped.Term} : N ↠β M → M =β N

instance SimplyTyped.instIsReflTermBetaEq : IsRefl SimplyTyped.Term fun (x1 x2 : SimplyTyped.Term) => x1 =β x2

Equations

• SimplyTyped.instIsReflTermBetaEq = ⋯

instance SimplyTyped.instIsSymmTermBetaEq : IsSymm SimplyTyped.Term fun (x1 x2 : SimplyTyped.Term) => x1 =β x2

Equations

• SimplyTyped.instIsSymmTermBetaEq = ⋯

instance SimplyTyped.instIsTransTermBetaEq : IsTrans SimplyTyped.Term fun (x1 x2 : SimplyTyped.Term) => x1 =β x2

Equations

• SimplyTyped.instIsTransTermBetaEq = ⋯

theorem SimplyTyped.church_rosser_corollary {M : SimplyTyped.Term} {N : SimplyTyped.Term} (h : M =β N) : ∃ (L : SimplyTyped.Term), M ↠β L ∧ N ↠β L

theorem SimplyTyped.subject_reduction {Γ : SimplyTyped.Context} {L : SimplyTyped.Term} {L' : SimplyTyped.Term} {ρ : SimplyTyped.Typ} (hj : Γ ⊢ L : ρ) (hb : L ↠β L') : Γ ⊢ L' : ρ