theorem
Auto.Embedding.Lam.LamValid.bvarLowers?
{lval : LamValuation}
{ss : List LamSort}
{lctx : Nat → LamSort}
{t : LamTerm}
{lvl : Nat}
{t' : LamTerm}
(hv : LamValid lval (pushLCtxs ss lctx) t)
(hlvl : ss.length = lvl)
(heq : LamTerm.bvarLowers? lvl t = some t')
(hInh : HList (LamNonempty lval.tyVal) ss)
:
LamValid lval lctx t'
theorem
Auto.Embedding.Lam.LamThmValid.bvarLowers?
{lval : LamValuation}
{ss lctx : List LamSort}
{t : LamTerm}
{lvl : Nat}
{t' : LamTerm}
(hv : LamThmValid lval (ss ++ lctx) t)
(hlvl : ss.length = lvl)
(heq : LamTerm.bvarLowers? lvl t = some t')
(hInh : HList (LamNonempty lval.tyVal) ss)
:
LamThmValid lval lctx t'
theorem
Auto.Embedding.Lam.LamValid.bvarLower?
{lval : LamValuation}
{s : LamSort}
{lctx : Nat → LamSort}
{t t' : LamTerm}
(hv : LamValid lval (pushLCtx s lctx) t)
(heq : t.bvarLower? = some t')
(hInh : LamNonempty lval.tyVal s)
:
LamValid lval lctx t'
theorem
Auto.Embedding.Lam.LamThmValid.bvarLower?
{lval : LamValuation}
{s : LamSort}
{lctx : List LamSort}
{t t' : LamTerm}
(hv : LamThmValid lval (s :: lctx) t)
(heq : t.bvarLower? = some t')
(hInh : LamNonempty lval.tyVal s)
:
LamThmValid lval lctx t'
Equations
Instances For
theorem
Auto.Embedding.Lam.LamTerm.maxEVarSucc_impApp?
{t₁₂ t₁ t' : LamTerm}
(heq : t₁₂.impApp? t₁ = some t')
:
theorem
Auto.Embedding.Lam.LamThmValid.impApp
{lval : LamValuation}
{lctx : List LamSort}
{t₁₂ t₁ res : LamTerm}
(H₁₂ : LamThmValid lval lctx t₁₂)
(H₁ : LamThmValid lval lctx t₁)
(heq : t₁₂.impApp? t₁ = some res)
:
LamThmValid lval lctx res
theorem
Auto.Embedding.Lam.LamThmValid.impApps
{lval : LamValuation}
{lctx : List LamSort}
{t : LamTerm}
{ps : List LamTerm}
{t' : LamTerm}
(vt : LamThmValid lval lctx t)
(vps : HList (LamThmValid lval lctx) ps)
(heq : t.impApps? ps = some t')
:
LamThmValid lval lctx t'
theorem
Auto.Embedding.Lam.LamThmValid.define
{s : LamSort}
{t : LamTerm}
{eidx : Nat}
{lval : LamValuation}
(wft : LamThmWF lval [] s t)
(heVar : t.maxEVarSucc ≤ eidx)
:
∃ (val : LamSort.interp lval.tyVal s), LamThmValid (lval.insertEVarAt s val eidx) [] (LamTerm.mkEq s (LamTerm.etom eidx) t)
theorem
Auto.Embedding.Lam.LamThmValid.skolemize
{lval : LamValuation}
{lctx : List LamSort}
{s : LamSort}
{p : LamTerm}
{eidx : Nat}
(vt : LamThmValid lval lctx (LamTerm.mkExistE s p))
(heVar : p.maxEVarSucc ≤ eidx)
:
∃ (val : LamSort.interp lval.tyVal (s.mkFuncsRev lctx)), LamThmValid (lval.insertEVarAt (s.mkFuncsRev lctx) val eidx) lctx
(LamTerm.app s p ((LamTerm.etom eidx).bvarApps lctx 0))
theorem
Auto.Embedding.Lam.LamThmValid.skolemize?
{lval : LamValuation}
{lctx : List LamSort}
{t : LamTerm}
{eidx : Nat}
{s : LamSort}
{t' : LamTerm}
(vt : LamThmValid lval lctx t)
(heq : t.skolemize? eidx lctx = some (s, t'))
(heVar : t.maxEVarSucc ≤ eidx)
:
∃ (val : LamSort.interp lval.tyVal (s.mkFuncsRev lctx)), LamThmValid (lval.insertEVarAt (s.mkFuncsRev lctx) val eidx) lctx t'