def Auto.Embedding.Lam.LamTerm.intro1F? (t : LamTerm) : Option (LamSort × LamTerm)

Equations

• (Auto.Embedding.Lam.LamTerm.app a (Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.forallE s)) (Auto.Embedding.Lam.LamTerm.lam a_1 t_2)).intro1F? = some (s, t_2)
• t.intro1F? = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_intro1F? {t : LamTerm} {s : LamSort} {t' : LamTerm} (heq : t.intro1F? = some (s, t')) : t'.maxEVarSucc = t.maxEVarSucc

theorem Auto.Embedding.Lam.LamValid.intro1F? {lval : LamValuation} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {p : LamTerm} (H : LamValid lval lctx t) (heq : t.intro1F? = some (s, p)) : LamValid lval (pushLCtx s lctx) p

theorem Auto.Embedding.Lam.LamThmValid.intro1F? {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} {s : LamSort} {p : LamTerm} (H : LamThmValid lval lctx t) (heq : t.intro1F? = some (s, p)) : LamThmValid lval (s :: lctx) p

First-order logic style intro1

def Auto.Embedding.Lam.LamTerm.intro1H? (t : LamTerm) : Option (LamSort × LamTerm)

Equations

• One or more equations did not get rendered due to their size.
• t.intro1H? = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_intro1H? {t : LamTerm} {s : LamSort} {t' : LamTerm} (heq : t.intro1H? = some (s, t')) : t'.maxEVarSucc = t.maxEVarSucc

theorem Auto.Embedding.Lam.LamValid.intro1H? {lval : LamValuation} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {p : LamTerm} (H : LamValid lval lctx t) (heq : t.intro1H? = some (s, p)) : LamValid lval (pushLCtx s lctx) p

theorem Auto.Embedding.Lam.LamThmValid.intro1H? {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} {s : LamSort} {p : LamTerm} (H : LamThmValid lval lctx t) (heq : t.intro1H? = some (s, p)) : LamThmValid lval (s :: lctx) p

Higher-order logic style intro1

def Auto.Embedding.Lam.LamTerm.intro1? (t : LamTerm) : Option (LamSort × LamTerm)

Equations

• One or more equations did not get rendered due to their size.
• (Auto.Embedding.Lam.LamTerm.app a (Auto.Embedding.Lam.LamTerm.base (Auto.Embedding.Lam.LamBaseTerm.forallE s)) (Auto.Embedding.Lam.LamTerm.lam a_1 t)).intro1? = some (s, t)
• t.intro1? = none

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_intro1? {t : LamTerm} {s : LamSort} {t' : LamTerm} (heq : t.intro1? = some (s, t')) : t'.maxEVarSucc = t.maxEVarSucc

theorem Auto.Embedding.Lam.LamValid.intro1? {lval : LamValuation} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {p : LamTerm} (H : LamValid lval lctx t) (heq : t.intro1? = some (s, p)) : LamValid lval (pushLCtx s lctx) p

theorem Auto.Embedding.Lam.LamThmValid.intro1? {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} {s : LamSort} {p : LamTerm} (H : LamThmValid lval lctx t) (heq : t.intro1? = some (s, p)) : LamThmValid lval (s :: lctx) p