def Auto.Embedding.Lam.LamTerm.mapBVarAt (idx : Nat) (f : Nat → Nat) (t : LamTerm) : LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.mapBVarAt idx f (Auto.Embedding.Lam.LamTerm.atom n) = Auto.Embedding.Lam.LamTerm.atom n
• Auto.Embedding.Lam.LamTerm.mapBVarAt idx f (Auto.Embedding.Lam.LamTerm.etom n) = Auto.Embedding.Lam.LamTerm.etom n
• Auto.Embedding.Lam.LamTerm.mapBVarAt idx f (Auto.Embedding.Lam.LamTerm.base b) = Auto.Embedding.Lam.LamTerm.base b
• Auto.Embedding.Lam.LamTerm.mapBVarAt idx f (Auto.Embedding.Lam.LamTerm.bvar n) = Auto.Embedding.Lam.LamTerm.bvar (Auto.Embedding.mapAt idx f n)
• Auto.Embedding.Lam.LamTerm.mapBVarAt idx f (Auto.Embedding.Lam.LamTerm.lam s t_2) = Auto.Embedding.Lam.LamTerm.lam s (Auto.Embedding.Lam.LamTerm.mapBVarAt idx.succ f t_2)

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_mapBVarAt {idx : Nat} {f : Nat → Nat} {t : LamTerm} : (mapBVarAt idx f t).maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamTerm.mapBVar (f : Nat → Nat) (t : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.mapBVar = Auto.Embedding.Lam.LamTerm.mapBVarAt 0

def Auto.Embedding.Lam.LamWF.mapBVarAt {f : Nat → Nat} {restore : (Nat → LamSort) → Nat → LamSort} {rty : LamSort} (covP : coPair f restore) (idx : Nat) {lamVarTy : LamTyVal} {lctx : Nat → LamSort} (rterm : LamTerm) (HWF : LamWF lamVarTy { lctx := lctx, rterm := rterm, rty := rty }) : LamWF lamVarTy { lctx := restoreAt idx restore lctx, rterm := LamTerm.mapBVarAt idx f rterm, rty := rty }

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamWF.mapBVarAt covP idx (Auto.Embedding.Lam.LamTerm.atom n) (Auto.Embedding.Lam.LamWF.ofAtom n) = Auto.Embedding.Lam.LamWF.ofAtom n
• Auto.Embedding.Lam.LamWF.mapBVarAt covP idx (Auto.Embedding.Lam.LamTerm.etom n) (Auto.Embedding.Lam.LamWF.ofEtom n) = Auto.Embedding.Lam.LamWF.ofEtom n
• Auto.Embedding.Lam.LamWF.mapBVarAt covP idx (Auto.Embedding.Lam.LamTerm.base b) (Auto.Embedding.Lam.LamWF.ofBase b_1) = Auto.Embedding.Lam.LamWF.ofBase b_1
• Auto.Embedding.Lam.LamWF.mapBVarAt covP idx (Auto.Embedding.Lam.LamTerm.bvar n) (Auto.Embedding.Lam.LamWF.ofBVar n) = ⋯ ▸ Auto.Embedding.Lam.LamWF.ofBVar (Auto.Embedding.mapAt idx f n)

def Auto.Embedding.Lam.LamWF.fromMapBVarAtAux {f : Nat → Nat} {restore : (Nat → LamSort) → Nat → LamSort} {lctx' : Nat → LamSort} {rterm' : LamTerm} {rty : LamSort} (covP : coPair f restore) (idx : Nat) {lamVarTy : LamTyVal} {lctx : Nat → LamSort} (rterm : LamTerm) (hLCtx : lctx' = restoreAt idx restore lctx) (hRTerm : rterm' = LamTerm.mapBVarAt idx f rterm) (HWF : LamWF lamVarTy { lctx := lctx', rterm := rterm', rty := rty }) : LamWF lamVarTy { lctx := lctx, rterm := rterm, rty := rty }

Equations

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

def Auto.Embedding.Lam.LamWF.fromMapBVarAt {f : Nat → Nat} {restore : (Nat → LamSort) → Nat → LamSort} {rty : LamSort} (covP : coPair f restore) (idx : Nat) {lamVarTy : LamTyVal} {lctx : Nat → LamSort} (rterm : LamTerm) (HWF : LamWF lamVarTy { lctx := restoreAt idx restore lctx, rterm := LamTerm.mapBVarAt idx f rterm, rty := rty }) : LamWF lamVarTy { lctx := lctx, rterm := rterm, rty := rty }

Equations

• Auto.Embedding.Lam.LamWF.fromMapBVarAt covP idx rterm HWF = Auto.Embedding.Lam.LamWF.fromMapBVarAtAux covP idx rterm ⋯ ⋯ HWF

theorem Auto.Embedding.Lam.LamWF.mapBVarAt.correct {f : Nat → Nat} {restore : (Nat → LamSort) → Nat → LamSort} {rTy : LamSort} (lval : LamValuation) {restoreDep : {rty : Nat → LamSort} → ((n : Nat) → LamSort.interp lval.tyVal (rty n)) → (n : Nat) → LamSort.interp lval.tyVal (restore rty n)} (covPD : coPairDep (LamSort.interp lval.tyVal) f restore restoreDep) (idx : Nat) {lctxTy : Nat → LamSort} (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) (rterm : LamTerm) (HWF : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := rterm, rty := rTy }) : interp lval lctxTy lctxTerm HWF = interp lval (restoreAt idx restore lctxTy) (restoreAtDep idx (fun {rty : Nat → LamSort} => restoreDep) lctxTerm) (mapBVarAt ⋯ idx rterm HWF)

def Auto.Embedding.Lam.LamTerm.bvarLiftsIdx (idx lvl : Nat) (t : LamTerm) : LamTerm

Changing all .bvar ?n in t (where ?n >= idx) to .bvar (?n + lvl)

Equations

• Auto.Embedding.Lam.LamTerm.bvarLiftsIdx idx lvl = Auto.Embedding.Lam.LamTerm.mapBVarAt idx fun (x : Nat) => x.add lvl

theorem Auto.Embedding.Lam.LamTerm.bvarLiftsIdx_eq_bvar {idx lvl : Nat} {t : LamTerm} {n : Nat} : bvarLiftsIdx idx lvl t = bvar n ↔ n < idx ∧ t = bvar n ∨ n ≥ idx + lvl ∧ t = bvar (n - lvl)

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_bvarLiftsIdx {idx lvl : Nat} {t : LamTerm} : (bvarLiftsIdx idx lvl t).maxEVarSucc = t.maxEVarSucc

@[reducible]

def Auto.Embedding.Lam.LamTerm.bvarLifts (lvl : Nat) (t : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.bvarLifts = Auto.Embedding.Lam.LamTerm.bvarLiftsIdx 0

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_bvarLifts {lvl : Nat} {t : LamTerm} : (bvarLifts lvl t).maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamTerm.bvarLiftIdx (idx : Nat) (t : LamTerm) : LamTerm

Changing all .bvar ?n in t (where ?n >= idx) to .bvar (Nat.succ ?n)

Equations

• Auto.Embedding.Lam.LamTerm.bvarLiftIdx idx t = Auto.Embedding.Lam.LamTerm.bvarLiftsIdx idx 1 t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_bvarLiftIdx {idx : Nat} {t : LamTerm} : (bvarLiftIdx idx t).maxEVarSucc = t.maxEVarSucc

@[reducible]

def Auto.Embedding.Lam.LamTerm.bvarLift (t : LamTerm) : LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.bvarLift = Auto.Embedding.Lam.LamTerm.bvarLiftIdx 0

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_bvarLift {t : LamTerm} : t.bvarLift.maxEVarSucc = t.maxEVarSucc

theorem Auto.Embedding.Lam.LamTerm.bvarLiftsIdx_atom {idx lvl n : Nat} : bvarLiftsIdx idx lvl (atom n) = atom n

theorem Auto.Embedding.Lam.LamTerm.bvarLiftIdx_atom {idx n : Nat} : bvarLiftIdx idx (atom n) = atom n

theorem Auto.Embedding.Lam.LamTerm.bvarLiftsIdx_etom {idx lvl n : Nat} : bvarLiftsIdx idx lvl (etom n) = etom n

theorem Auto.Embedding.Lam.LamTerm.bvarLiftIdx_etom {idx n : Nat} : bvarLiftIdx idx (etom n) = etom n

theorem Auto.Embedding.Lam.LamTerm.bvarLiftsIdx_base {idx lvl : Nat} {b : LamBaseTerm} : bvarLiftsIdx idx lvl (base b) = base b

theorem Auto.Embedding.Lam.LamTerm.bvarLiftIdx_base {idx : Nat} {b : LamBaseTerm} : bvarLiftIdx idx (base b) = base b

theorem Auto.Embedding.Lam.LamTerm.bvarLiftsIdx_bvar {idx lvl n : Nat} : bvarLiftsIdx idx lvl (bvar n) = bvar (mapAt idx (fun (x : Nat) => x + lvl) n)

theorem Auto.Embedding.Lam.LamTerm.bvarLiftIdx_bvar {idx n : Nat} : bvarLiftIdx idx (bvar n) = bvar (mapAt idx (fun (x : Nat) => x.succ) n)

theorem Auto.Embedding.Lam.LamTerm.bvarLiftsIdx_app {idx lvl : Nat} {s : LamSort} {fn arg : LamTerm} : bvarLiftsIdx idx lvl (app s fn arg) = app s (bvarLiftsIdx idx lvl fn) (bvarLiftsIdx idx lvl arg)

theorem Auto.Embedding.Lam.LamTerm.bvarLiftIdx_app {idx : Nat} {s : LamSort} {fn arg : LamTerm} : bvarLiftIdx idx (app s fn arg) = app s (bvarLiftIdx idx fn) (bvarLiftIdx idx arg)

theorem Auto.Embedding.Lam.LamTerm.bvarLiftsIdx_lam {idx lvl : Nat} {s : LamSort} {body : LamTerm} : bvarLiftsIdx idx lvl (lam s body) = lam s (bvarLiftsIdx idx.succ lvl body)

theorem Auto.Embedding.Lam.LamTerm.bvarLiftIdx_lam {idx : Nat} {s : LamSort} {body : LamTerm} : bvarLiftIdx idx (lam s body) = lam s (bvarLiftIdx idx.succ body)

theorem Auto.Embedding.Lam.LamTerm.bvarLiftsIdx_zero (idx : Nat) (t : LamTerm) : bvarLiftsIdx idx 0 t = t

theorem Auto.Embedding.Lam.LamTerm.bvarLifts_zero {t : LamTerm} : bvarLifts 0 t = t

theorem Auto.Embedding.Lam.LamTerm.bvarLiftsIdx_succ_l (idx lvl : Nat) (t : LamTerm) : bvarLiftsIdx idx lvl.succ t = bvarLiftsIdx idx lvl (bvarLiftIdx idx t)

theorem Auto.Embedding.Lam.LamTerm.bvarLifts_succ_l {lvl : Nat} {t : LamTerm} : bvarLifts lvl.succ t = bvarLifts lvl t.bvarLift

theorem Auto.Embedding.Lam.LamTerm.bvarLiftsIdx_succ_r (idx lvl : Nat) (t : LamTerm) : bvarLiftsIdx idx lvl.succ t = bvarLiftIdx idx (bvarLiftsIdx idx lvl t)

theorem Auto.Embedding.Lam.LamTerm.bvarLifts_succ_r {lvl : Nat} {t : LamTerm} : bvarLifts lvl.succ t = (bvarLifts lvl t).bvarLift

theorem Auto.Embedding.Lam.LamTerm.bvarLifts_add {idx lvl₁ lvl₂ : Nat} {t : LamTerm} : bvarLiftsIdx idx (lvl₁ + lvl₂) t = bvarLiftsIdx idx lvl₁ (bvarLiftsIdx idx lvl₂ t)

def Auto.Embedding.Lam.LamWF.bvarLiftsIdx {rTy : LamSort} {lamVarTy : LamTyVal} {lctx : Nat → LamSort} {idx lvl : Nat} {xs : List LamSort} (heq : xs.length = lvl) (rterm : LamTerm) (HWF : LamWF lamVarTy { lctx := lctx, rterm := rterm, rty := rTy }) : LamWF lamVarTy { lctx := pushLCtxsAt xs idx lctx, rterm := LamTerm.bvarLiftsIdx idx lvl rterm, rty := rTy }

Equations

• Auto.Embedding.Lam.LamWF.bvarLiftsIdx heq rterm HWF = Auto.Embedding.Lam.LamWF.mapBVarAt ⋯ idx rterm HWF

def Auto.Embedding.Lam.LamWF.fromBVarLiftsIdx {rTy : LamSort} {lamVarTy : LamTyVal} {lctx : Nat → LamSort} {idx lvl : Nat} {xs : List LamSort} (heq : xs.length = lvl) (rterm : LamTerm) (HWF : LamWF lamVarTy { lctx := pushLCtxsAt xs idx lctx, rterm := LamTerm.bvarLiftsIdx idx lvl rterm, rty := rTy }) : LamWF lamVarTy { lctx := lctx, rterm := rterm, rty := rTy }

Equations

• Auto.Embedding.Lam.LamWF.fromBVarLiftsIdx heq rterm HWF = Auto.Embedding.Lam.LamWF.fromMapBVarAt ⋯ idx rterm HWF

theorem Auto.Embedding.Lam.LamWF.interp_bvarLiftsIdx {rTy : LamSort} (lval : LamValuation) {idx lvl : Nat} {tys : List LamSort} (xs : HList (LamSort.interp lval.tyVal) tys) (heq : tys.length = lvl) (lctxTy : Nat → LamSort) (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) (rterm : LamTerm) (HWF : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := rterm, rty := rTy }) : interp lval lctxTy lctxTerm HWF = interp lval (pushLCtxsAt tys idx lctxTy) (pushLCtxsAtDep xs idx lctxTerm) (bvarLiftsIdx heq rterm HWF)

def Auto.Embedding.Lam.LamWF.bvarLifts {rTy : LamSort} {lamVarTy : LamTyVal} {lctx : Nat → LamSort} {lvl : Nat} {xs : List LamSort} (heq : xs.length = lvl) (rterm : LamTerm) (HWF : LamWF lamVarTy { lctx := lctx, rterm := rterm, rty := rTy }) : LamWF lamVarTy { lctx := pushLCtxs xs lctx, rterm := LamTerm.bvarLifts lvl rterm, rty := rTy }

Equations

• Auto.Embedding.Lam.LamWF.bvarLifts heq rterm HWF = ⋯.mp (Auto.Embedding.Lam.LamWF.bvarLiftsIdx heq rterm HWF)

def Auto.Embedding.Lam.LamWF.fromBVarLifts {rTy : LamSort} {lamVarTy : LamTyVal} {lctx : Nat → LamSort} {lvl : Nat} {xs : List LamSort} (heq : xs.length = lvl) (rterm : LamTerm) (HWF : LamWF lamVarTy { lctx := pushLCtxs xs lctx, rterm := LamTerm.bvarLifts lvl rterm, rty := rTy }) : LamWF lamVarTy { lctx := lctx, rterm := rterm, rty := rTy }

Equations

• Auto.Embedding.Lam.LamWF.fromBVarLifts heq rterm HWF = Auto.Embedding.Lam.LamWF.fromBVarLiftsIdx heq rterm (⋯.mp HWF)

theorem Auto.Embedding.Lam.LamWF.interp_bvarLifts {rTy : LamSort} (lval : LamValuation) {lvl : Nat} {tys : List LamSort} (xs : HList (LamSort.interp lval.tyVal) tys) (heq : tys.length = lvl) (lctxTy : Nat → LamSort) (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) (rterm : LamTerm) (HWF : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := rterm, rty := rTy }) : interp lval lctxTy lctxTerm HWF = interp lval (pushLCtxs tys lctxTy) (pushLCtxsDep xs lctxTerm) (bvarLifts heq rterm HWF)

def Auto.Embedding.Lam.LamWF.bvarLiftIdx {rTy s : LamSort} {lamVarTy : LamTyVal} {lctx : Nat → LamSort} (idx : Nat) (rterm : LamTerm) (HWF : LamWF lamVarTy { lctx := lctx, rterm := rterm, rty := rTy }) : LamWF lamVarTy { lctx := pushLCtxAt s idx lctx, rterm := LamTerm.bvarLiftIdx idx rterm, rty := rTy }

Equations

• Auto.Embedding.Lam.LamWF.bvarLiftIdx idx rterm HWF = Auto.Embedding.Lam.LamWF.mapBVarAt ⋯ idx rterm HWF

def Auto.Embedding.Lam.LamWF.fromBVarLiftIdx {s rTy : LamSort} {lamVarTy : LamTyVal} {lctx : Nat → LamSort} (idx : Nat) (rterm : LamTerm) (HWF : LamWF lamVarTy { lctx := pushLCtxAt s idx lctx, rterm := LamTerm.bvarLiftIdx idx rterm, rty := rTy }) : LamWF lamVarTy { lctx := lctx, rterm := rterm, rty := rTy }

Equations

• Auto.Embedding.Lam.LamWF.fromBVarLiftIdx idx rterm HWF = Auto.Embedding.Lam.LamWF.fromMapBVarAt ⋯ idx rterm HWF

theorem Auto.Embedding.Lam.LamWF.interp_bvarLiftIdx {rTy : LamSort} (lval : LamValuation) {idx : Nat} (lctxTy : Nat → LamSort) (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) {xty : LamSort} (x : LamSort.interp lval.tyVal xty) (rterm : LamTerm) (HWF : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := rterm, rty := rTy }) : interp lval lctxTy lctxTerm HWF = interp lval (pushLCtxAt xty idx lctxTy) (pushLCtxAtDep x idx lctxTerm) (bvarLiftIdx idx rterm HWF)

def Auto.Embedding.Lam.LamWF.bvarLift {rTy s : LamSort} {lamVarTy : LamTyVal} {lctx : Nat → LamSort} (rterm : LamTerm) (HWF : LamWF lamVarTy { lctx := lctx, rterm := rterm, rty := rTy }) : LamWF lamVarTy { lctx := pushLCtx s lctx, rterm := rterm.bvarLift, rty := rTy }

Equations

• Auto.Embedding.Lam.LamWF.bvarLift rterm HWF = ⋯.mp (Auto.Embedding.Lam.LamWF.bvarLiftIdx 0 rterm HWF)

def Auto.Embedding.Lam.LamWF.fromBVarLift {s rTy : LamSort} {lamVarTy : LamTyVal} {lctx : Nat → LamSort} (rterm : LamTerm) (HWF : LamWF lamVarTy { lctx := pushLCtx s lctx, rterm := rterm.bvarLift, rty := rTy }) : LamWF lamVarTy { lctx := lctx, rterm := rterm, rty := rTy }

Equations

• Auto.Embedding.Lam.LamWF.fromBVarLift rterm HWF = Auto.Embedding.Lam.LamWF.fromBVarLiftIdx 0 rterm (⋯.mp HWF)

theorem Auto.Embedding.Lam.LamWF.interp_bvarLift {rTy : LamSort} (lval : LamValuation) (lctxTy : Nat → LamSort) (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) {xty : LamSort} (x : LamSort.interp lval.tyVal xty) (rterm : LamTerm) (HWF : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := rterm, rty := rTy }) : interp lval lctxTy lctxTerm HWF = interp lval (pushLCtx xty lctxTy) (pushLCtxDep x lctxTerm) (bvarLift rterm HWF)

def Auto.Embedding.Lam.LamWF.pushLCtxAt_ofBVar {lamVarTy : LamTyVal} {s : LamSort} {idx : Nat} {lctx : Nat → LamSort} : LamWF lamVarTy { lctx := pushLCtxAt s idx lctx, rterm := LamTerm.bvar idx, rty := s }

Equations

• Auto.Embedding.Lam.LamWF.pushLCtxAt_ofBVar = ⋯.mp (Auto.Embedding.Lam.LamWF.ofBVar idx)

def Auto.Embedding.Lam.LamWF.pushLCtx_ofBVar {lamVarTy : LamTyVal} {s : LamSort} {lctx : Nat → LamSort} : LamWF lamVarTy { lctx := pushLCtx s lctx, rterm := LamTerm.bvar 0, rty := s }

Equations

• Auto.Embedding.Lam.LamWF.pushLCtx_ofBVar = ⋯.mp (Auto.Embedding.Lam.LamWF.ofBVar 0)

def Auto.Embedding.Lam.LamTerm.bvarLowersIdx? (idx lvl : Nat) : LamTerm → Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.bvarLowersIdx? idx lvl (Auto.Embedding.Lam.LamTerm.atom n) = some (Auto.Embedding.Lam.LamTerm.atom n)
• Auto.Embedding.Lam.LamTerm.bvarLowersIdx? idx lvl (Auto.Embedding.Lam.LamTerm.etom n) = some (Auto.Embedding.Lam.LamTerm.etom n)
• Auto.Embedding.Lam.LamTerm.bvarLowersIdx? idx lvl (Auto.Embedding.Lam.LamTerm.base b) = some (Auto.Embedding.Lam.LamTerm.base b)

theorem Auto.Embedding.Lam.LamTerm.bvarLowersIdx?_bvar_eq_some {idx lvl n : Nat} {t : LamTerm} : bvarLowersIdx? idx lvl (bvar n) = some t ↔ n < idx ∧ t = bvar n ∨ n ≥ idx + lvl ∧ t = bvar (n - lvl)

theorem Auto.Embedding.Lam.LamTerm.bvarLowersIdx?_spec {idx lvl : Nat} {t t' : LamTerm} : bvarLowersIdx? idx lvl t = some t' ↔ bvarLiftsIdx idx lvl t' = t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_bvarLowersIdx? {idx lvl : Nat} {t t' : LamTerm} (heq : bvarLowersIdx? idx lvl t = some t') : t'.maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamTerm.bvarLowers? (lvl : Nat) (t : LamTerm) : Option LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.bvarLowers? lvl t = Auto.Embedding.Lam.LamTerm.bvarLowersIdx? 0 lvl t

theorem Auto.Embedding.Lam.LamTerm.bvarLowers?_spec {lvl : Nat} {t t' : LamTerm} : bvarLowers? lvl t = some t' ↔ bvarLifts lvl t' = t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_bvarLowers? {lvl : Nat} {t t' : LamTerm} (heq : bvarLowers? lvl t = some t') : t'.maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamTerm.bvarLowerIdx? (idx : Nat) (t : LamTerm) : Option LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.bvarLowerIdx? idx t = Auto.Embedding.Lam.LamTerm.bvarLowersIdx? idx 1 t

theorem Auto.Embedding.Lam.LamTerm.bvarLowerIdx?_spec {idx : Nat} {t t' : LamTerm} : bvarLowerIdx? idx t = some t' ↔ bvarLiftIdx idx t' = t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_bvarLowerIdx? {idx : Nat} {t t' : LamTerm} (heq : bvarLowerIdx? idx t = some t') : t'.maxEVarSucc = t.maxEVarSucc

def Auto.Embedding.Lam.LamTerm.bvarLower? (t : LamTerm) : Option LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.bvarLower? = Auto.Embedding.Lam.LamTerm.bvarLowerIdx? 0

theorem Auto.Embedding.Lam.LamTerm.bvarLower?_spec {t t' : LamTerm} : t.bvarLower? = some t' ↔ t'.bvarLift = t

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_bvarLower? {t t' : LamTerm} (heq : t.bvarLower? = some t') : t'.maxEVarSucc = t.maxEVarSucc

partial def Auto.Embedding.Lam.LamTerm.toStringLCtx (lctx : Nat) : LamTerm → String

def Auto.Embedding.Lam.LamTerm.toString : LamTerm → String

Equations

• Auto.Embedding.Lam.LamTerm.toString = Auto.Embedding.Lam.LamTerm.toStringLCtx 0

instance Auto.Embedding.Lam.instToStringLamTerm : ToString LamTerm

Equations

• Auto.Embedding.Lam.instToStringLamTerm = { toString := Auto.Embedding.Lam.LamTerm.toString }