@[reducible]

def Auto.Embedding.Lam.dfLCtxTy : Nat → LamSort

Equations

• Auto.Embedding.Lam.dfLCtxTy x✝ = Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop

@[reducible]

def Auto.Embedding.Lam.dfLCtxTerm (val : Nat → Type u) (n : Nat) : LamSort.interp val (dfLCtxTy n)

Equations

• Auto.Embedding.Lam.dfLCtxTerm val x✝ = { down := False }

def Auto.Embedding.Lam.LamNonempty (tyVal : Nat → Type u) (s : LamSort) : Prop

Equations

• Auto.Embedding.Lam.LamNonempty tyVal s = Nonempty (Auto.Embedding.Lam.LamSort.interp tyVal s)

def Auto.Embedding.Lam.LamWF.generalizeTy {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} (wf : LamWF ltv { lctx := lctx, rterm := t, rty := s }) : (s : LamSort) × LamWF ltv { lctx := lctx, rterm := t, rty := s }

Equations

• wf.generalizeTy = ⟨s, wf⟩

def Auto.Embedding.Lam.LamThmWF (lval : LamValuation) (lctx : List LamSort) (rty : LamSort) (t : LamTerm) : Type

Equations

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

def Auto.Embedding.Lam.LamThmWFP (lval : LamValuation) (lctx : List LamSort) (rty : LamSort) (t : LamTerm) : Prop

Equations

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

def Auto.Embedding.Lam.LamThmWFD (lval : LamValuation) (lctx : List LamSort) (rty : LamSort) (t : LamTerm) : Prop

Equations

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

@[reducible, inline]

abbrev Auto.Embedding.Lam.LamValid (lval : LamValuation) (lctx : Nat → LamSort) (t : LamTerm) : Prop

Equations

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

def Auto.Embedding.Lam.LamThmValid (lval : LamValuation) (lctx : List LamSort) (t : LamTerm) : Prop

Equations

• Auto.Embedding.Lam.LamThmValid lval lctx t = ∀ (lctx' : Nat → Auto.Embedding.Lam.LamSort), Auto.Embedding.Lam.LamValid lval (Auto.Embedding.pushLCtxs lctx lctx') t

def Auto.Embedding.Lam.LamThmValidD (lval : LamValuation) (lctx : List LamSort) (t : LamTerm) : Prop

Equations

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

@[reducible, inline]

abbrev Auto.Embedding.Lam.LamEquiv (lval : LamValuation) (lctx : Nat → LamSort) (rty : LamSort) (t₁ t₂ : LamTerm) : Prop

Equations

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

def Auto.Embedding.Lam.LamThmEquiv (lval : LamValuation) (lctx : List LamSort) (rty : LamSort) (t₁ t₂ : LamTerm) : Prop

Equations

• Auto.Embedding.Lam.LamThmEquiv lval lctx rty t₁ t₂ = ∀ (lctx' : Nat → Auto.Embedding.Lam.LamSort), Auto.Embedding.Lam.LamEquiv lval (Auto.Embedding.pushLCtxs lctx lctx') rty t₁ t₂

def Auto.Embedding.Lam.LamGenEquiv (lval : LamValuation) (t₁ t₂ : LamTerm) : Prop

Equations

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

def Auto.Embedding.Lam.LamGenEquivWith (lval : LamValuation) (rty : LamSort) (t₁ t₂ : LamTerm) : Prop

Equations

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

def Auto.Embedding.Lam.LamGenConv (lval : LamValuation) (conv : LamTerm → Option LamTerm) : Prop

Generic conversions like clausification satisfy LamGenConv

Equations

• Auto.Embedding.Lam.LamGenConv lval conv = ∀ (t₁ t₂ : Auto.Embedding.Lam.LamTerm), conv t₁ = some t₂ → Auto.Embedding.Lam.LamGenEquiv lval t₁ t₂

def Auto.Embedding.Lam.LamGenConvWith (lval : LamValuation) (conv : LamSort → LamTerm → Option LamTerm) : Prop

Generic conversions like eta expansion satisfy LamGenConvWith

Equations

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

def Auto.Embedding.Lam.LamGenModify (lval : LamValuation) (modify : LamTerm → Option LamTerm) (weaken? : Bool) : Prop

Equations

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

def Auto.Embedding.Lam.LamTerm.getPos (occ : List Bool) (t : LamTerm) : Option LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.getPos [] t = some t
• Auto.Embedding.Lam.LamTerm.getPos (b :: occ_2) (Auto.Embedding.Lam.LamTerm.lam a body) = Auto.Embedding.Lam.LamTerm.getPos occ_2 body
• Auto.Embedding.Lam.LamTerm.getPos (false :: occ_2) (Auto.Embedding.Lam.LamTerm.app a fn arg) = Auto.Embedding.Lam.LamTerm.getPos occ_2 fn
• Auto.Embedding.Lam.LamTerm.getPos (true :: occ_2) (Auto.Embedding.Lam.LamTerm.app a fn arg) = Auto.Embedding.Lam.LamTerm.getPos occ_2 arg
• Auto.Embedding.Lam.LamTerm.getPos (b :: occ_2) t = none

def Auto.Embedding.Lam.LamTerm.rwGenAt (occ : List Bool) (conv : LamTerm → Option LamTerm) (t : LamTerm) : Option LamTerm

Apply conversion theorem at a given position in t The conversion should only be ones that satisfy LamGenConv

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.rwGenAt [] conv t = conv t
• Auto.Embedding.Lam.LamTerm.rwGenAt (b :: occ_2) conv t = none

def Auto.Embedding.Lam.LamTerm.rwGenAll (conv : LamTerm → Option LamTerm) (t : LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.rwGenAll conv t = match conv t with | some t' => some t' | none => some t

theorem Auto.Embedding.Lam.LamTerm.rwGenAll_atom {conv : LamTerm → Option LamTerm} {n : Nat} : rwGenAll conv (atom n) = some ((conv (atom n)).getD (atom n))

theorem Auto.Embedding.Lam.LamTerm.rwGenAll_etom {conv : LamTerm → Option LamTerm} {n : Nat} : rwGenAll conv (etom n) = some ((conv (etom n)).getD (etom n))

theorem Auto.Embedding.Lam.LamTerm.rwGenAll_base {conv : LamTerm → Option LamTerm} {b : LamBaseTerm} : rwGenAll conv (base b) = some ((conv (base b)).getD (base b))

theorem Auto.Embedding.Lam.LamTerm.rwGenAll_bvar {conv : LamTerm → Option LamTerm} {n : Nat} : rwGenAll conv (bvar n) = some ((conv (bvar n)).getD (bvar n))

theorem Auto.Embedding.Lam.LamTerm.rwGenAll_lam {conv : LamTerm → Option LamTerm} {s : LamSort} {body : LamTerm} : rwGenAll conv (lam s body) = match conv (lam s body) with | some t' => some t' | none => (rwGenAll conv body).bind fun (x : LamTerm) => some (lam s x)

theorem Auto.Embedding.Lam.LamTerm.rwGenAll_app {conv : LamTerm → Option LamTerm} {s : LamSort} {fn arg : LamTerm} : rwGenAll conv (app s fn arg) = match conv (app s fn arg) with | some t' => some t' | none => match rwGenAll conv fn, rwGenAll conv arg with | some fn', some arg' => some (app s fn' arg') | x, x_1 => none

def Auto.Embedding.Lam.LamTerm.getPosWith (occ : List Bool) (rty : LamSort) (t : LamTerm) : Option (LamSort × LamTerm)

Equations

• Auto.Embedding.Lam.LamTerm.getPosWith [] rty t = some (rty, t)
• Auto.Embedding.Lam.LamTerm.getPosWith (b :: occ_2) (a_1.func resTy) (Auto.Embedding.Lam.LamTerm.lam a body) = Auto.Embedding.Lam.LamTerm.getPosWith occ_2 resTy body
• Auto.Embedding.Lam.LamTerm.getPosWith (b :: occ_2) rty (Auto.Embedding.Lam.LamTerm.lam a body) = none
• Auto.Embedding.Lam.LamTerm.getPosWith (false :: occ_2) rty (Auto.Embedding.Lam.LamTerm.app a fn arg) = Auto.Embedding.Lam.LamTerm.getPosWith occ_2 (a.func rty) fn
• Auto.Embedding.Lam.LamTerm.getPosWith (true :: occ_2) rty (Auto.Embedding.Lam.LamTerm.app a fn arg) = Auto.Embedding.Lam.LamTerm.getPosWith occ_2 a arg
• Auto.Embedding.Lam.LamTerm.getPosWith (b :: occ_2) rty t = none

def Auto.Embedding.Lam.LamTerm.rwGenAtWith (occ : List Bool) (conv : LamSort → LamTerm → Option LamTerm) (rty : LamSort) (t : LamTerm) : Option LamTerm

Apply conversion theorem at a given position in t The conversion should only be ones that satisfy LamGenConvWith

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.rwGenAtWith [] conv rty t = conv rty t
• Auto.Embedding.Lam.LamTerm.rwGenAtWith (b :: occ_2) conv rty (Auto.Embedding.Lam.LamTerm.lam a body) = none
• Auto.Embedding.Lam.LamTerm.rwGenAtWith (b :: occ_2) conv rty t = none

def Auto.Embedding.Lam.LamTerm.rwGenAllWith (conv : LamSort → LamTerm → Option LamTerm) (rty : LamSort) (t : LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.rwGenAllWith conv rty (Auto.Embedding.Lam.LamTerm.lam a body) = match conv rty (Auto.Embedding.Lam.LamTerm.lam a body) with | some t' => some t' | none => none
• Auto.Embedding.Lam.LamTerm.rwGenAllWith conv rty t = match conv rty t with | some t' => some t' | none => some t

@[reducible]

def Auto.Embedding.Lam.LamTerm.evarEquiv (conv : LamTerm → Option LamTerm) : Prop

Equations

• Auto.Embedding.Lam.LamTerm.evarEquiv conv = ∀ (t t' : Auto.Embedding.Lam.LamTerm), conv t = some t' → t'.maxEVarSucc = t.maxEVarSucc

@[reducible]

def Auto.Embedding.Lam.LamTerm.evarBounded (conv : LamTerm → Option LamTerm) (bound : Nat) : Prop

Equations

• Auto.Embedding.Lam.LamTerm.evarBounded conv bound = ∀ (t t' : Auto.Embedding.Lam.LamTerm), conv t = some t' → t'.maxEVarSucc ≤ max bound t.maxEVarSucc

theorem Auto.Embedding.Lam.LamTerm.rwGenAllWith_atom {conv : LamSort → LamTerm → Option LamTerm} {s : LamSort} {n : Nat} : rwGenAllWith conv s (atom n) = some ((conv s (atom n)).getD (atom n))

theorem Auto.Embedding.Lam.LamTerm.rwGenAllWith_etom {conv : LamSort → LamTerm → Option LamTerm} {s : LamSort} {n : Nat} : rwGenAllWith conv s (etom n) = some ((conv s (etom n)).getD (etom n))

theorem Auto.Embedding.Lam.LamTerm.rwGenAllWith_base {conv : LamSort → LamTerm → Option LamTerm} {s : LamSort} {b : LamBaseTerm} : rwGenAllWith conv s (base b) = some ((conv s (base b)).getD (base b))

theorem Auto.Embedding.Lam.LamTerm.rwGenAllWith_bvar {conv : LamSort → LamTerm → Option LamTerm} {s : LamSort} {n : Nat} : rwGenAllWith conv s (bvar n) = some ((conv s (bvar n)).getD (bvar n))

theorem Auto.Embedding.Lam.LamTerm.rwGenAllWith_lam {conv : LamSort → LamTerm → Option LamTerm} {rty s : LamSort} {body : LamTerm} : rwGenAllWith conv rty (lam s body) = match conv rty (lam s body) with | some t' => some t' | none => match rty with | a.func resTy => (rwGenAllWith conv resTy body).bind fun (x : LamTerm) => some (lam s x) | x => none

theorem Auto.Embedding.Lam.LamTerm.rwGenAllWith_app {conv : LamSort → LamTerm → Option LamTerm} {rty s : LamSort} {fn arg : LamTerm} : rwGenAllWith conv rty (app s fn arg) = match conv rty (app s fn arg) with | some t' => some t' | none => match rwGenAllWith conv (s.func rty) fn, rwGenAllWith conv s arg with | some fn', some arg' => some (app s fn' arg') | x, x_1 => none

def Auto.Embedding.Lam.LamTerm.isSign (sign : Bool) (occ : List Bool) (t : LamTerm) : Bool

Determine whether a position is negative / whether a position is positive

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.isSign sign [] t = sign
• Auto.Embedding.Lam.LamTerm.isSign sign (b :: occ_2) t = false

def Auto.Embedding.Lam.LamTerm.rwGenAtIfSign (sign : Bool) (occ : List Bool) (conv : LamTerm → Option LamTerm) (t : LamTerm) : Option LamTerm

Equations

• Auto.Embedding.Lam.LamTerm.rwGenAtIfSign sign occ conv t = match Auto.Embedding.Lam.LamTerm.isSign sign occ t with | true => Auto.Embedding.Lam.LamTerm.rwGenAt occ conv t | false => none

noncomputable def Auto.Embedding.Lam.LamNonempty.get {tyVal : Nat → Type u_1} {s : LamSort} (h : LamNonempty tyVal s) : LamSort.interp tyVal s

Equations

• h.get = Classical.choice h

theorem Auto.Embedding.Lam.LamValid_substLCtxRecWF {lctx : Nat → LamSort} {t : LamTerm} {lval : LamValuation} (lctx' : Nat → LamSort) (heq : ∀ (n : Nat), lctx' n = lctx n) {wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := LamSort.base LamBaseSort.prop }} : (∀ (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctx n)), (LamWF.interp lval lctx lctxTerm wf).down) ↔ ∀ (lctxTerm' : (n : Nat) → LamSort.interp lval.tyVal (lctx' n)), (LamWF.interp lval lctx' lctxTerm' (⋯ ▸ wf)).down

@[irreducible]

def Auto.Embedding.Lam.LamWF.ofExistsLamWF {ltv : LamTyVal} {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {p : Prop} (H : ∃ (x : LamWF ltv { lctx := lctx, rterm := t, rty := s }), p) : LamWF ltv { lctx := lctx, rterm := t, rty := s }

Equations

• Auto.Embedding.Lam.LamWF.ofExistsLamWF H = Auto.Embedding.Lam.LamWF.ofNonemptyLamWF ⋯

@[irreducible]

def Auto.Embedding.Lam.LamThmWF.ofLamThmWFP {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} (H : LamThmWFP lval lctx s t) : LamThmWF lval lctx s t

Equations

• Auto.Embedding.Lam.LamThmWF.ofLamThmWFP H lctx' = Auto.Embedding.Lam.LamWF.ofNonemptyLamWF ⋯

theorem Auto.Embedding.Lam.LamThmWFP.ofLamThmWF {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} (H : LamThmWF lval lctx s t) : LamThmWFP lval lctx s t

def Auto.Embedding.Lam.LamTerm.lamThmWFCheck? (ltv : LamTyVal) (lctx : List LamSort) (t : LamTerm) : Option LamSort

Equations

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

theorem Auto.Embedding.Lam.LamTerm.lamThmWFCheck?_spec {ltv : LamTyVal} {lctx : List LamSort} {t : LamTerm} {rty : LamSort} (H : lamThmWFCheck? ltv lctx t = some rty) : lamCheck? ltv (pushLCtxs lctx dfLCtxTy) t = some rty ∧ t.maxLooseBVarSucc ≤ lctx.length

@[irreducible]

def Auto.Embedding.Lam.LamThmWF.ofLamThmWFCheck? {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t : LamTerm} (h : LamTerm.lamThmWFCheck? lval.toLamTyVal lctx t = some rty) : LamThmWF lval lctx rty t

Equations

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

@[irreducible]

def Auto.Embedding.Lam.LamThmWF.ofLamThmValid {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} (H : LamThmValid lval lctx t) : LamThmWF lval lctx (LamSort.base LamBaseSort.prop) t

Equations

• Auto.Embedding.Lam.LamThmWF.ofLamThmValid H = Auto.Embedding.Lam.LamThmWF.ofLamThmWFP ⋯

theorem Auto.Embedding.Lam.LamThmWF.maxLooseBVarSucc {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t : LamTerm} (H : LamThmWF lval lctx rty t) : t.maxLooseBVarSucc ≤ lctx.length

theorem Auto.Embedding.Lam.LamThmValid.maxLooseBVarSucc {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} (H : LamThmValid lval lctx t) : t.maxLooseBVarSucc ≤ lctx.length

theorem Auto.Embedding.Lam.LamThmWFD.ofLamThmWF {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t : LamTerm} (H : LamThmWF lval lctx rty t) : LamThmWFD lval lctx rty t

@[irreducible]

def Auto.Embedding.Lam.LamThmWF.ofLamThmWFD {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t : LamTerm} (H : LamThmWFD lval lctx rty t) : LamThmWF lval lctx rty t

Equations

• Auto.Embedding.Lam.LamThmWF.ofLamThmWFD H = Auto.Embedding.Lam.LamThmWF.ofLamThmWFP ⋯

theorem Auto.Embedding.Lam.LamValid.eVarIrrelevance (lval₁ lval₂ : LamValuation) {lctxTy₁ lctxTy₂ : Nat → LamSort} {t : LamTerm} (hLamVarTy : lval₁.lamVarTy = lval₂.lamVarTy) (hLamILTy : lval₁.lamILTy = lval₂.lamILTy) (hTyVal : lval₁.tyVal ≍ lval₂.tyVal) (hVarVal : lval₁.varVal ≍ lval₂.varVal) (hILVal : lval₁.ilVal ≍ lval₂.ilVal) (hLCtxTy : lctxTy₁ = lctxTy₂) (hirr : ∀ (n : Nat), n < t.maxEVarSucc → lval₁.lamEVarTy n = lval₂.lamEVarTy n ∧ lval₁.eVarVal n ≍ lval₂.eVarVal n) (hValid : LamValid lval₁ lctxTy₁ t) : LamValid lval₂ lctxTy₂ t

theorem Auto.Embedding.Lam.LamThmValidD.ofLamThmValid {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} (H : LamThmValid lval lctx t) : LamThmValidD lval lctx t

theorem Auto.Embedding.Lam.LamThmValid.ofLamThmValidD {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} (H : LamThmValidD lval lctx t) : LamThmValid lval lctx t

theorem Auto.Embedding.Lam.LamThmValid.eVarIrrelevance (lval₁ lval₂ : LamValuation) {lctx₁ lctx₂ : List LamSort} {t : LamTerm} (hLamVarTy : lval₁.lamVarTy = lval₂.lamVarTy) (hLamILTy : lval₁.lamILTy = lval₂.lamILTy) (hTyVal : lval₁.tyVal ≍ lval₂.tyVal) (hVarVal : lval₁.varVal ≍ lval₂.varVal) (hILVal : lval₁.ilVal ≍ lval₂.ilVal) (hLCtxTy : lctx₁ = lctx₂) (hirr : ∀ (n : Nat), n < t.maxEVarSucc → lval₁.lamEVarTy n = lval₂.lamEVarTy n ∧ lval₁.eVarVal n ≍ lval₂.eVarVal n) : LamThmValid lval₁ lctx₁ t → LamThmValid lval₂ lctx₂ t

@[irreducible]

def Auto.Embedding.Lam.LamThmWF.ofLamThmEquiv_l {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t₁ t₂ : LamTerm} (teq : LamThmEquiv lval lctx rty t₁ t₂) : LamThmWF lval lctx rty t₁

Equations

• Auto.Embedding.Lam.LamThmWF.ofLamThmEquiv_l teq = Auto.Embedding.Lam.LamThmWF.ofLamThmWFP ⋯

@[irreducible]

def Auto.Embedding.Lam.LamThmWF.ofLamThmEquiv_r {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t₁ t₂ : LamTerm} (teq : LamThmEquiv lval lctx rty t₁ t₂) : LamThmWF lval lctx rty t₂

Equations

• Auto.Embedding.Lam.LamThmWF.ofLamThmEquiv_r teq = Auto.Embedding.Lam.LamThmWF.ofLamThmWFP ⋯

theorem Auto.Embedding.Lam.LamValid.ofLamEquiv {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {t₁ t₂ : LamTerm} (leq : LamEquiv lval lctx s t₁ t₂) : LamValid lval lctx (LamTerm.mkEq s t₁ t₂)

theorem Auto.Embedding.Lam.LamThmValid.ofLamThmEquiv {lval : LamValuation} {s : LamSort} {t₁ t₂ : LamTerm} (lctx : List LamSort) (eT : LamThmEquiv lval lctx s t₁ t₂) : LamThmValid lval lctx (LamTerm.mkEq s t₁ t₂)

def Auto.Embedding.Lam.LamThmWF.append {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t : LamTerm} (H : LamThmWF lval lctx rty t) (ex : List LamSort) : LamThmWF lval (lctx ++ ex) rty t

Equations

• H.append ex = id fun (lctx' : Nat → Auto.Embedding.Lam.LamSort) => ⋯.mpr (H (Auto.Embedding.pushLCtxs ex lctx'))

def Auto.Embedding.Lam.LamThmWF.prepend {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {t : LamTerm} (H : LamThmWF lval lctx rty t) (ex : List LamSort) : LamThmWF lval (ex ++ lctx) rty (LamTerm.bvarLifts ex.length t)

Equations

• H.prepend ex = id fun (lctx' : Nat → Auto.Embedding.Lam.LamSort) => ⋯.mpr (⋯.mpr (Auto.Embedding.Lam.LamWF.bvarLiftsIdx ⋯ t (H lctx')))

theorem Auto.Embedding.Lam.LamValid.revert1F {lval : LamValuation} {s : LamSort} {lctx : Nat → LamSort} {t : LamTerm} (H : LamValid lval (pushLCtx s lctx) t) : LamValid lval lctx (LamTerm.mkForallEF s t)

theorem Auto.Embedding.Lam.LamThmValid.revert1F {lval : LamValuation} {s : LamSort} {lctx : List LamSort} {t : LamTerm} (H : LamThmValid lval (s :: lctx) t) : LamThmValid lval lctx (LamTerm.mkForallEF s t)

theorem Auto.Embedding.Lam.LamValid.intro1F {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {t : LamTerm} (H : LamValid lval lctx (LamTerm.mkForallEF s t)) : LamValid lval (pushLCtx s lctx) t

theorem Auto.Embedding.Lam.LamThmValid.intro1F {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} (H : LamThmValid lval lctx (LamTerm.mkForallEF s t)) : LamThmValid lval (s :: lctx) t

theorem Auto.Embedding.Lam.LamValid.eqForallEF {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {t : LamTerm} : LamValid lval lctx (LamTerm.mkForallEF s t) ↔ LamValid lval (pushLCtx s lctx) t

theorem Auto.Embedding.Lam.LamThmValid.eqForallEF {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} : LamThmValid lval lctx (LamTerm.mkForallEF s t) ↔ LamThmValid lval (s :: lctx) t

theorem Auto.Embedding.Lam.LamWF.interp_eqForallEH {lctx : Nat → LamSort} {t : LamTerm} {argTy : LamSort} {lval : LamValuation} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctx n)} {wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := argTy.func (LamSort.base LamBaseSort.prop) }} : (interp lval lctx lctxTerm wf.mkForallE).down = ∀ (x : LamSort.interp lval.tyVal argTy), (interp lval (pushLCtx argTy lctx) (pushLCtxDep x lctxTerm) (ofApp argTy (bvarLift t wf) pushLCtx_ofBVar)).down

theorem Auto.Embedding.Lam.LamValid.revert1H {lval : LamValuation} {s : LamSort} {lctx : Nat → LamSort} {t : LamTerm} (H : LamValid lval (pushLCtx s lctx) (LamTerm.app s t.bvarLift (LamTerm.bvar 0))) : LamValid lval lctx (LamTerm.mkForallE s t)

theorem Auto.Embedding.Lam.LamThmValid.revert1H {lval : LamValuation} {s : LamSort} {lctx : List LamSort} {t : LamTerm} (H : LamThmValid lval (s :: lctx) (LamTerm.app s t.bvarLift (LamTerm.bvar 0))) : LamThmValid lval lctx (LamTerm.mkForallE s t)

theorem Auto.Embedding.Lam.LamValid.intro1H {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {t : LamTerm} (H : LamValid lval lctx (LamTerm.mkForallE s t)) : LamValid lval (pushLCtx s lctx) (LamTerm.app s t.bvarLift (LamTerm.bvar 0))

theorem Auto.Embedding.Lam.LamThmValid.intro1H {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} (H : LamThmValid lval lctx (LamTerm.mkForallE s t)) : LamThmValid lval (s :: lctx) (LamTerm.app s t.bvarLift (LamTerm.bvar 0))

theorem Auto.Embedding.Lam.LamValid.eqForallEH {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {t : LamTerm} : LamValid lval lctx (LamTerm.mkForallE s t) ↔ LamValid lval (pushLCtx s lctx) (LamTerm.app s t.bvarLift (LamTerm.bvar 0))

theorem Auto.Embedding.Lam.LamThmValid.eqForallEH {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} : LamThmValid lval lctx (LamTerm.mkForallE s t) ↔ LamThmValid lval (s :: lctx) (LamTerm.app s t.bvarLift (LamTerm.bvar 0))

theorem Auto.Embedding.Lam.LamValid.eqForallEFN {lval : LamValuation} {lctx : Nat → LamSort} {t : LamTerm} {l : List LamSort} : LamValid lval lctx (t.mkForallEFN l) ↔ LamValid lval (pushLCtxs l.reverse lctx) t

theorem Auto.Embedding.Lam.LamValid.eqForallEFN' {lval : LamValuation} {lctx : Nat → LamSort} {t : LamTerm} {l : List LamSort} : LamValid lval lctx (t.mkForallEFN l.reverse) ↔ LamValid lval (pushLCtxs l lctx) t

theorem Auto.Embedding.Lam.LamThmValid.eqForallEFN {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} {l : List LamSort} : LamThmValid lval lctx (t.mkForallEFN l) ↔ LamThmValid lval (l.reverse ++ lctx) t

theorem Auto.Embedding.Lam.LamThmValid.eqForallEFN' {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} {l : List LamSort} : LamThmValid lval lctx (t.mkForallEFN l.reverse) ↔ LamThmValid lval (l ++ lctx) t

theorem Auto.Embedding.Lam.LamThmValid.append {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} (H : LamThmValid lval lctx t) (ex : List LamSort) : LamThmValid lval (lctx ++ ex) t

theorem Auto.Embedding.Lam.LamValid.prepend {lval : LamValuation} {lctx : Nat → LamSort} {t : LamTerm} (H : LamValid lval lctx t) (ex : List LamSort) : LamValid lval (pushLCtxs ex lctx) (LamTerm.bvarLifts ex.length t)

theorem Auto.Embedding.Lam.LamThmValid.prepend {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} (H : LamThmValid lval lctx t) (ex : List LamSort) : LamThmValid lval (ex ++ lctx) (LamTerm.bvarLifts ex.length t)

theorem Auto.Embedding.Lam.LamEquiv.ofLamValid {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {t₁ t₂ : LamTerm} (heq : LamValid lval lctx (LamTerm.mkEq s t₁ t₂)) : LamEquiv lval lctx s t₁ t₂

theorem Auto.Embedding.Lam.LamEquiv.ofLamValidSymm {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {t₁ t₂ : LamTerm} (heq : LamValid lval lctx (LamTerm.mkEq s t₁ t₂)) : LamEquiv lval lctx s t₂ t₁

theorem Auto.Embedding.Lam.LamThmEquiv.ofLamThmValid {lval : LamValuation} {s : LamSort} {t₁ t₂ : LamTerm} (lctx : List LamSort) (heq : LamThmValid lval lctx (LamTerm.mkEq s t₁ t₂)) : LamThmEquiv lval lctx s t₁ t₂

theorem Auto.Embedding.Lam.LamEquiv.eqLamValid {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {t₁ t₂ : LamTerm} : LamEquiv lval lctx s t₁ t₂ = LamValid lval lctx (LamTerm.mkEq s t₁ t₂)

theorem Auto.Embedding.Lam.LamThmEquiv.eqLamThmValid {lval : LamValuation} {s : LamSort} {t₁ t₂ : LamTerm} (lctx : List LamSort) : LamThmEquiv lval lctx s t₁ t₂ = LamThmValid lval lctx (LamTerm.mkEq s t₁ t₂)

theorem Auto.Embedding.Lam.LamValid.mpLamEquiv {lval : LamValuation} {lctx : Nat → LamSort} {p₁ : LamTerm} {s : LamSort} {p₂ : LamTerm} (hp : LamValid lval lctx p₁) (hequiv : LamEquiv lval lctx s p₁ p₂) : LamValid lval lctx p₂

theorem Auto.Embedding.Lam.LamThmValid.mpLamThmEquiv {lval : LamValuation} {lctx : List LamSort} {p₁ p₂ : LamTerm} (hequiv : LamThmEquiv lval lctx (LamSort.base LamBaseSort.prop) p₁ p₂) (hp : LamThmValid lval lctx p₁) : LamThmValid lval lctx p₂

theorem Auto.Embedding.Lam.LamEquiv.refl {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {lval : LamValuation} (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) : LamEquiv lval lctx s t t

theorem Auto.Embedding.Lam.LamThmEquiv.refl {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t : LamTerm} (wf : LamThmWF lval lctx s t) : LamThmEquiv lval lctx s t t

theorem Auto.Embedding.Lam.LamGenEquiv.refl {lval : LamValuation} {t : LamTerm} : LamGenEquiv lval t t

theorem Auto.Embedding.Lam.LamGenEquivWith.refl {lval : LamValuation} {s : LamSort} {t : LamTerm} : LamGenEquivWith lval s t t

theorem Auto.Embedding.Lam.LamEquiv.eq {lctx : Nat → LamSort} {t₁ : LamTerm} {s : LamSort} {t₂ : LamTerm} {lval : LamValuation} (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t₁, rty := s }) (heq : t₁ = t₂) : LamEquiv lval lctx s t₁ t₂

theorem Auto.Embedding.Lam.LamThmEquiv.eq {lval : LamValuation} {lctx : List LamSort} {s : LamSort} {t₁ t₂ : LamTerm} (wf : LamThmWF lval lctx s t₁) (heq : t₁ = t₂) : LamThmEquiv lval lctx s t₁ t₂

theorem Auto.Embedding.Lam.LamGenEquiv.eq {t₁ t₂ : LamTerm} {lval : LamValuation} (heq : t₁ = t₂) : LamGenEquiv lval t₁ t₂

theorem Auto.Embedding.Lam.LamEquiv.symm {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {a b : LamTerm} (e : LamEquiv lval lctx s a b) : LamEquiv lval lctx s b a

theorem Auto.Embedding.Lam.LamThmEquiv.symm {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {a b : LamTerm} (e : LamThmEquiv lval lctx rty a b) : LamThmEquiv lval lctx rty b a

theorem Auto.Embedding.Lam.LamEquiv.trans {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {a b c : LamTerm} (eab : LamEquiv lval lctx s a b) (ebc : LamEquiv lval lctx s b c) : LamEquiv lval lctx s a c

theorem Auto.Embedding.Lam.LamEquiv.trans' {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {a b : LamTerm} {s' : LamSort} {c : LamTerm} (eab : LamEquiv lval lctx s a b) (ebc : LamEquiv lval lctx s' b c) : LamEquiv lval lctx s a c

theorem Auto.Embedding.Lam.LamThmEquiv.trans {lval : LamValuation} {lctx : List LamSort} {rty : LamSort} {a b c : LamTerm} (e₁ : LamThmEquiv lval lctx rty a b) (e₂ : LamThmEquiv lval lctx rty b c) : LamThmEquiv lval lctx rty a c

theorem Auto.Embedding.Lam.LamEquiv.ofLam {lval : LamValuation} {w : LamSort} {lctx : Nat → LamSort} {s : LamSort} {a b : LamTerm} (e : LamEquiv lval (pushLCtx w lctx) s a b) : LamEquiv lval lctx (w.func s) (LamTerm.lam w a) (LamTerm.lam w b)

theorem Auto.Embedding.Lam.LamThmEquiv.ofLam {lval : LamValuation} {w : LamSort} {lctx : List LamSort} {s : LamSort} {a b : LamTerm} (e : LamThmEquiv lval (w :: lctx) s a b) : LamThmEquiv lval lctx (w.func s) (LamTerm.lam w a) (LamTerm.lam w b)

theorem Auto.Embedding.Lam.LamGenEquiv.ofLam {lval : LamValuation} {a b : LamTerm} {w : LamSort} (e : LamGenEquiv lval a b) : LamGenEquiv lval (LamTerm.lam w a) (LamTerm.lam w b)

theorem Auto.Embedding.Lam.LamGenEquivWith.ofLam {lval : LamValuation} {s : LamSort} {a b : LamTerm} {w'' w : LamSort} (e : LamGenEquivWith lval s a b) : LamGenEquivWith lval (w''.func s) (LamTerm.lam w a) (LamTerm.lam w b)

theorem Auto.Embedding.Lam.LamEquiv.fromLam {lval : LamValuation} {lctx : Nat → LamSort} {w s : LamSort} {a b : LamTerm} (e : LamEquiv lval lctx (w.func s) (LamTerm.lam w a) (LamTerm.lam w b)) : LamEquiv lval (pushLCtx w lctx) s a b

theorem Auto.Embedding.Lam.LamThmEquiv.fromLam {lval : LamValuation} {lctx : List LamSort} {w s : LamSort} {a b : LamTerm} (e : LamThmEquiv lval lctx (w.func s) (LamTerm.lam w a) (LamTerm.lam w b)) : LamThmEquiv lval (w :: lctx) s a b

theorem Auto.Embedding.Lam.LamEquiv.eqLam {lval : LamValuation} {w : LamSort} {lctx : Nat → LamSort} {s : LamSort} {a b : LamTerm} : LamEquiv lval (pushLCtx w lctx) s a b = LamEquiv lval lctx (w.func s) (LamTerm.lam w a) (LamTerm.lam w b)

theorem Auto.Embedding.Lam.LamThmEquiv.eqLam {lval : LamValuation} {w : LamSort} {lctx : List LamSort} {s : LamSort} {a b : LamTerm} : LamThmEquiv lval (w :: lctx) s a b = LamThmEquiv lval lctx (w.func s) (LamTerm.lam w a) (LamTerm.lam w b)

theorem Auto.Embedding.Lam.LamEquiv.congr {lval : LamValuation} {lctx : Nat → LamSort} {argTy resTy : LamSort} {fn₁ fn₂ arg₁ arg₂ : LamTerm} (eFn : LamEquiv lval lctx (argTy.func resTy) fn₁ fn₂) (eArg : LamEquiv lval lctx argTy arg₁ arg₂) : LamEquiv lval lctx resTy (LamTerm.app argTy fn₁ arg₁) (LamTerm.app argTy fn₂ arg₂)

theorem Auto.Embedding.Lam.LamThmEquiv.congr {lval : LamValuation} {lctx : List LamSort} {argTy resTy : LamSort} {fn₁ fn₂ arg₁ arg₂ : LamTerm} (eFn : LamThmEquiv lval lctx (argTy.func resTy) fn₁ fn₂) (eArg : LamThmEquiv lval lctx argTy arg₁ arg₂) : LamThmEquiv lval lctx resTy (LamTerm.app argTy fn₁ arg₁) (LamTerm.app argTy fn₂ arg₂)

theorem Auto.Embedding.Lam.LamGenEquiv.congr {lval : LamValuation} {fn₁ fn₂ arg₁ arg₂ : LamTerm} {argTy : LamSort} (eFn : LamGenEquiv lval fn₁ fn₂) (eArg : LamGenEquiv lval arg₁ arg₂) : LamGenEquiv lval (LamTerm.app argTy fn₁ arg₁) (LamTerm.app argTy fn₂ arg₂)

theorem Auto.Embedding.Lam.LamGenEquivWith.congr {lval : LamValuation} {argTy resTy : LamSort} {fn₁ fn₂ arg₁ arg₂ : LamTerm} (eFn : LamGenEquivWith lval (argTy.func resTy) fn₁ fn₂) (eArg : LamGenEquivWith lval argTy arg₁ arg₂) : LamGenEquivWith lval resTy (LamTerm.app argTy fn₁ arg₁) (LamTerm.app argTy fn₂ arg₂)

theorem Auto.Embedding.Lam.LamEquiv.congrFun {lval : LamValuation} {lctx : Nat → LamSort} {argTy resTy : LamSort} {fn₁ fn₂ arg : LamTerm} (eFn : LamEquiv lval lctx (argTy.func resTy) fn₁ fn₂) (wfArg : LamWF lval.toLamTyVal { lctx := lctx, rterm := arg, rty := argTy }) : LamEquiv lval lctx resTy (LamTerm.app argTy fn₁ arg) (LamTerm.app argTy fn₂ arg)

theorem Auto.Embedding.Lam.LamThmEquiv.congrFun {lval : LamValuation} {lctx : List LamSort} {argTy resTy : LamSort} {fn₁ fn₂ arg : LamTerm} (eFn : LamThmEquiv lval lctx (argTy.func resTy) fn₁ fn₂) (wfArg : LamThmWF lval lctx argTy arg) : LamThmEquiv lval lctx resTy (LamTerm.app argTy fn₁ arg) (LamTerm.app argTy fn₂ arg)

theorem Auto.Embedding.Lam.LamGenEquiv.congrFun {lval : LamValuation} {fn₁ fn₂ : LamTerm} {s : LamSort} {arg : LamTerm} (eFn : LamGenEquiv lval fn₁ fn₂) : LamGenEquiv lval (LamTerm.app s fn₁ arg) (LamTerm.app s fn₂ arg)

theorem Auto.Embedding.Lam.LamGenEquivWith.congrFun {lval : LamValuation} {s resTy : LamSort} {fn₁ fn₂ arg : LamTerm} (eFn : LamGenEquivWith lval (s.func resTy) fn₁ fn₂) : LamGenEquivWith lval resTy (LamTerm.app s fn₁ arg) (LamTerm.app s fn₂ arg)

theorem Auto.Embedding.Lam.LamEquiv.congrArg {lctx : Nat → LamSort} {fn : LamTerm} {argTy resTy : LamSort} {lval : LamValuation} {arg₁ arg₂ : LamTerm} (wfFn : LamWF lval.toLamTyVal { lctx := lctx, rterm := fn, rty := argTy.func resTy }) (eArg : LamEquiv lval lctx argTy arg₁ arg₂) : LamEquiv lval lctx resTy (LamTerm.app argTy fn arg₁) (LamTerm.app argTy fn arg₂)

theorem Auto.Embedding.Lam.LamThmEquiv.congrArg {lval : LamValuation} {lctx : List LamSort} {argTy resTy : LamSort} {fn arg₁ arg₂ : LamTerm} (wfFn : LamThmWF lval lctx (argTy.func resTy) fn) (eArg : LamThmEquiv lval lctx argTy arg₁ arg₂) : LamThmEquiv lval lctx resTy (LamTerm.app argTy fn arg₁) (LamTerm.app argTy fn arg₂)

theorem Auto.Embedding.Lam.LamGenEquiv.congrArg {lval : LamValuation} {arg₁ arg₂ : LamTerm} {s : LamSort} {fn : LamTerm} (eArg : LamGenEquiv lval arg₁ arg₂) : LamGenEquiv lval (LamTerm.app s fn arg₁) (LamTerm.app s fn arg₂)

theorem Auto.Embedding.Lam.LamGenEquivWith.congrArg {lval : LamValuation} {s : LamSort} {arg₁ arg₂ : LamTerm} {resTy : LamSort} {fn : LamTerm} (eArg : LamGenEquivWith lval s arg₁ arg₂) : LamGenEquivWith lval resTy (LamTerm.app s fn arg₁) (LamTerm.app s fn arg₂)

theorem Auto.Embedding.Lam.LamEquiv.congr_mkLamFN {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {t₁ t₂ : LamTerm} {l : List LamSort} : LamEquiv lval (pushLCtxs l.reverse lctx) s t₁ t₂ ↔ LamEquiv lval lctx (s.mkFuncs l) (t₁.mkLamFN l) (t₂.mkLamFN l)

theorem Auto.Embedding.Lam.LamEquiv.congrs {lctx : Nat → LamSort} {fn₁ : LamTerm} {resTy : LamSort} {lval : LamValuation} {fnTy : LamSort} {fn₂ : LamTerm} {args : List (LamSort × LamTerm × LamTerm)} (wfApp : LamWF lval.toLamTyVal { lctx := lctx, rterm := fn₁.mkAppN (List.map (fun (x : LamSort × LamTerm × LamTerm) => match x with | (s, t₁, snd) => (s, t₁)) args), rty := resTy }) (hFn : LamEquiv lval lctx fnTy fn₁ fn₂) (hArgs : HList (fun (x : LamSort × LamTerm × LamTerm) => match x with | (s, arg₁, arg₂) => LamEquiv lval lctx s arg₁ arg₂) args) : LamEquiv lval lctx resTy (fn₁.mkAppN (List.map (fun (x : LamSort × LamTerm × LamTerm) => match x with | (s, t₁, snd) => (s, t₁)) args)) (fn₂.mkAppN (List.map (fun (x : LamSort × LamTerm × LamTerm) => match x with | (s, fst, t₂) => (s, t₂)) args))

theorem Auto.Embedding.Lam.LamEquiv.congrArgs {lctx : Nat → LamSort} {fn : LamTerm} {resTy : LamSort} {lval : LamValuation} {args : List (LamSort × LamTerm × LamTerm)} (wfApp : LamWF lval.toLamTyVal { lctx := lctx, rterm := fn.mkAppN (List.map (fun (x : LamSort × LamTerm × LamTerm) => match x with | (s, t₁, snd) => (s, t₁)) args), rty := resTy }) (hArgs : HList (fun (x : LamSort × LamTerm × LamTerm) => match x with | (s, arg₁, arg₂) => LamEquiv lval lctx s arg₁ arg₂) args) : LamEquiv lval lctx resTy (fn.mkAppN (List.map (fun (x : LamSort × LamTerm × LamTerm) => match x with | (s, t₁, snd) => (s, t₁)) args)) (fn.mkAppN (List.map (fun (x : LamSort × LamTerm × LamTerm) => match x with | (s, fst, t₂) => (s, t₂)) args))

theorem Auto.Embedding.Lam.LamEquiv.congrFunN {lctx : Nat → LamSort} {fn₁ : LamTerm} {resTy : LamSort} {lval : LamValuation} {fnTy : LamSort} {fn₂ : LamTerm} {args : List (LamSort × LamTerm)} (wfApp : LamWF lval.toLamTyVal { lctx := lctx, rterm := fn₁.mkAppN args, rty := resTy }) (hFn : LamEquiv lval lctx fnTy fn₁ fn₂) : LamEquiv lval lctx resTy (fn₁.mkAppN args) (fn₂.mkAppN args)

theorem Auto.Embedding.Lam.LamEquiv.forall_congr {lval : LamValuation} {argTy : LamSort} {lctx : Nat → LamSort} {fn₁ fn₂ : LamTerm} (eFn : LamEquiv lval (pushLCtx argTy lctx) (LamSort.base LamBaseSort.prop) fn₁ fn₂) : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (LamTerm.mkForallEF argTy fn₁) (LamTerm.mkForallEF argTy fn₂)

theorem Auto.Embedding.Lam.LamEquiv.congr_mkForallEFN {lval : LamValuation} {lctx : Nat → LamSort} {t₁ t₂ : LamTerm} {l : List LamSort} (H : LamEquiv lval (pushLCtxs l.reverse lctx) (LamSort.base LamBaseSort.prop) t₁ t₂) : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (t₁.mkForallEFN l) (t₂.mkForallEFN l)

theorem Auto.Embedding.Lam.LamEquiv.congr_mkForallEFN' {lval : LamValuation} {l : List LamSort} {lctx : Nat → LamSort} {t₁ t₂ : LamTerm} (H : LamEquiv lval (pushLCtxs l lctx) (LamSort.base LamBaseSort.prop) t₁ t₂) : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (t₁.mkForallEFN l.reverse) (t₂.mkForallEFN l.reverse)

theorem Auto.Embedding.Lam.LamEquiv.not_imp_not {lctx : Nat → LamSort} {t₁ t₂ : LamTerm} {lval : LamValuation} (wf₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := t₁, rty := LamSort.base LamBaseSort.prop }) (wf₂ : LamWF lval.toLamTyVal { lctx := lctx, rterm := t₂, rty := LamSort.base LamBaseSort.prop }) : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (t₁.mkNot.mkImp t₂.mkNot) (t₂.mkImp t₁)

theorem Auto.Embedding.Lam.LamEquiv.imp_swap {lctx : Nat → LamSort} {t₁ t₂ t₃ : LamTerm} {lval : LamValuation} (wf₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := t₁, rty := LamSort.base LamBaseSort.prop }) (wf₂ : LamWF lval.toLamTyVal { lctx := lctx, rterm := t₂, rty := LamSort.base LamBaseSort.prop }) (wf₃ : LamWF lval.toLamTyVal { lctx := lctx, rterm := t₃, rty := LamSort.base LamBaseSort.prop }) : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (t₁.mkImp (t₂.mkImp t₃)) (t₂.mkImp (t₁.mkImp t₃))

theorem Auto.Embedding.Lam.LamValid.eq_refl {lctx : Nat → LamSort} {a : LamTerm} {s : LamSort} {lval : LamValuation} (wfA : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := s }) : LamValid lval lctx (LamTerm.mkEq s a a)

theorem Auto.Embedding.Lam.LamValid.eq_eq {a b : LamTerm} {lctx : Nat → LamSort} {s : LamSort} {lval : LamValuation} (heq : a = b) (wfA : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := s }) : LamValid lval lctx (LamTerm.mkEq s a b)

theorem Auto.Embedding.Lam.LamValid.eq_symm {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {a b : LamTerm} (H : LamValid lval lctx (LamTerm.mkEq s a b)) : LamValid lval lctx (LamTerm.mkEq s b a)

theorem Auto.Embedding.Lam.LamValid.eq_trans {lval : LamValuation} {lctx : Nat → LamSort} {s : LamSort} {a b c : LamTerm} (H₁ : LamValid lval lctx (LamTerm.mkEq s a b)) (H₂ : LamValid lval lctx (LamTerm.mkEq s b c)) : LamValid lval lctx (LamTerm.mkEq s a c)

theorem Auto.Embedding.Lam.LamValid.eq_congr {lval : LamValuation} {lctx : Nat → LamSort} {argTy resTy : LamSort} {fn₁ fn₂ arg₁ arg₂ : LamTerm} (HFn : LamValid lval lctx (LamTerm.mkEq (argTy.func resTy) fn₁ fn₂)) (HArg : LamValid lval lctx (LamTerm.mkEq argTy arg₁ arg₂)) : LamValid lval lctx (LamTerm.mkEq resTy (LamTerm.app argTy fn₁ arg₁) (LamTerm.app argTy fn₂ arg₂))

theorem Auto.Embedding.Lam.LamValid.eq_congrFun {lval : LamValuation} {lctx : Nat → LamSort} {argTy resTy : LamSort} {fn₁ fn₂ arg : LamTerm} (HFn : LamValid lval lctx (LamTerm.mkEq (argTy.func resTy) fn₁ fn₂)) (wfArg₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := arg, rty := argTy }) : LamValid lval lctx (LamTerm.mkEq resTy (LamTerm.app argTy fn₁ arg) (LamTerm.app argTy fn₂ arg))

theorem Auto.Embedding.Lam.LamValid.eq_congrArg {lval : LamValuation} {lctx : Nat → LamSort} {argTy : LamSort} {arg₁ arg₂ fn : LamTerm} {resTy : LamSort} (HArg : LamValid lval lctx (LamTerm.mkEq argTy arg₁ arg₂)) (wfFn₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := fn, rty := argTy.func resTy }) : LamValid lval lctx (LamTerm.mkEq resTy (LamTerm.app argTy fn arg₁) (LamTerm.app argTy fn arg₂))

def Auto.Embedding.Lam.LamWF.funextF {ltv : LamTyVal} {lctx : Nat → LamSort} {argTy resTy : LamSort} {fn₁ fn₂ : LamTerm} {s : LamSort} (wf : LamWF ltv { lctx := lctx, rterm := LamTerm.mkEq (argTy.func resTy) fn₁ fn₂, rty := s }) : LamWF ltv { lctx := pushLCtx argTy lctx, rterm := LamTerm.mkEq resTy (LamTerm.app argTy fn₁.bvarLift (LamTerm.bvar 0)) (LamTerm.app argTy fn₂.bvarLift (LamTerm.bvar 0)), rty := LamSort.base LamBaseSort.prop }

Equations

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

def Auto.Embedding.Lam.LamWF.ofFunextF {ltv : LamTyVal} {argTy : LamSort} {lctx : Nat → LamSort} {resTy s : LamSort} {fn₁ fn₂ : LamTerm} (wf : LamWF ltv { lctx := pushLCtx argTy lctx, rterm := LamTerm.mkEq resTy (LamTerm.app argTy fn₁.bvarLift (LamTerm.bvar 0)) (LamTerm.app argTy fn₂.bvarLift (LamTerm.bvar 0)), rty := s }) : LamWF ltv { lctx := lctx, rterm := LamTerm.mkEq (argTy.func resTy) fn₁ fn₂, rty := LamSort.base LamBaseSort.prop }

Equations

• wf.ofFunextF = (Auto.Embedding.Lam.LamWF.fromBVarLift fn₁ wf.getFn.getArg.getFn).mkEq (Auto.Embedding.Lam.LamWF.fromBVarLift fn₂ wf.getArg.getFn)

theorem Auto.Embedding.Lam.LamWF.interp_funext {lctx : Nat → LamSort} {argTy resTy : LamSort} {fn₁ fn₂ : LamTerm} {lval : LamValuation} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctx n)} {wf₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := LamTerm.mkEq (argTy.func resTy) fn₁ fn₂, rty := LamSort.base LamBaseSort.prop }} {wf₂ : LamWF lval.toLamTyVal { lctx := pushLCtx argTy lctx, rterm := LamTerm.mkEq resTy (LamTerm.app argTy fn₁.bvarLift (LamTerm.bvar 0)) (LamTerm.app argTy fn₂.bvarLift (LamTerm.bvar 0)), rty := LamSort.base LamBaseSort.prop }} : (interp lval lctx lctxTerm wf₁).down = ∀ (x : LamSort.interp lval.tyVal argTy), (interp lval (pushLCtx argTy lctx) (pushLCtxDep x lctxTerm) wf₂).down

theorem Auto.Embedding.Lam.LamEquiv.eqFunextF {lctx : Nat → LamSort} {argTy resTy : LamSort} {fn₁ fn₂ : LamTerm} {s : LamSort} {lval : LamValuation} (wfEq : LamWF lval.toLamTyVal { lctx := lctx, rterm := LamTerm.mkEq (argTy.func resTy) fn₁ fn₂, rty := s }) : LamEquiv lval lctx s (LamTerm.mkEq (argTy.func resTy) fn₁ fn₂) (LamTerm.mkForallEF argTy (LamTerm.mkEq resTy (LamTerm.app argTy fn₁.bvarLift (LamTerm.bvar 0)) (LamTerm.app argTy fn₂.bvarLift (LamTerm.bvar 0))))

theorem Auto.Embedding.Lam.LamEquiv.eqFunextH {argTy : LamSort} {lctx : Nat → LamSort} {resTy : LamSort} {p₁ p₂ : LamTerm} {s : LamSort} {lval : LamValuation} (wfEq : LamWF lval.toLamTyVal { lctx := pushLCtx argTy lctx, rterm := LamTerm.mkEq resTy p₁ p₂, rty := s }) : LamEquiv lval lctx s (LamTerm.mkForallEF argTy (LamTerm.mkEq resTy p₁ p₂)) (LamTerm.mkEq (argTy.func resTy) (LamTerm.lam argTy p₁) (LamTerm.lam argTy p₂))

theorem Auto.Embedding.Lam.LamEquiv.funextF {lval : LamValuation} {argTy : LamSort} {lctx : Nat → LamSort} {resTy : LamSort} {fn₁ fn₂ : LamTerm} (eAp : LamEquiv lval (pushLCtx argTy lctx) resTy (LamTerm.app argTy fn₁.bvarLift (LamTerm.bvar 0)) (LamTerm.app argTy fn₂.bvarLift (LamTerm.bvar 0))) : LamEquiv lval lctx (argTy.func resTy) fn₁ fn₂

theorem Auto.Embedding.Lam.LamValid.funextF {lval : LamValuation} {argTy : LamSort} {lctx : Nat → LamSort} {resTy : LamSort} {fn₁ fn₂ : LamTerm} (HApp : LamValid lval (pushLCtx argTy lctx) (LamTerm.mkEq resTy (LamTerm.app argTy fn₁.bvarLift (LamTerm.bvar 0)) (LamTerm.app argTy fn₂.bvarLift (LamTerm.bvar 0)))) : LamValid lval lctx (LamTerm.mkEq (argTy.func resTy) fn₁ fn₂)

theorem Auto.Embedding.Lam.LamValid.impLift {lval : LamValuation} {lctx : Nat → LamSort} {t₁ t₂ : LamTerm} (H : LamValid lval lctx (t₁.mkImp t₂)) : LamValid lval lctx t₁ → LamValid lval lctx t₂

theorem Auto.Embedding.Lam.LamValid.imp_self {lctx : Nat → LamSort} {t : LamTerm} {lval : LamValuation} (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := LamSort.base LamBaseSort.prop }) : LamValid lval lctx (t.mkImp t)

theorem Auto.Embedding.Lam.LamThmValid.imp_self {lval : LamValuation} {lctx : List LamSort} {t : LamTerm} (wf : LamThmWF lval lctx (LamSort.base LamBaseSort.prop) t) : LamThmValid lval lctx (t.mkImp t)

theorem Auto.Embedding.Lam.LamValid.imp_trans {lctx : Nat → LamSort} {a b c : LamTerm} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.prop }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.prop }) (wfc : LamWF lval.toLamTyVal { lctx := lctx, rterm := c, rty := LamSort.base LamBaseSort.prop }) : LamValid lval lctx ((a.mkImp b).mkImp ((b.mkImp c).mkImp (a.mkImp c)))

theorem Auto.Embedding.Lam.LamValid.imp_trans' {lctx : Nat → LamSort} {a b c : LamTerm} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.prop }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.prop }) (wfc : LamWF lval.toLamTyVal { lctx := lctx, rterm := c, rty := LamSort.base LamBaseSort.prop }) : LamValid lval lctx ((b.mkImp c).mkImp ((a.mkImp b).mkImp (a.mkImp c)))

theorem Auto.Embedding.Lam.LamValid.and_imp_and_of_imp_imp {lctx : Nat → LamSort} {a₁ a₂ b₁ b₂ : LamTerm} {lval : LamValuation} (wfa₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := a₁, rty := LamSort.base LamBaseSort.prop }) (wfa₂ : LamWF lval.toLamTyVal { lctx := lctx, rterm := a₂, rty := LamSort.base LamBaseSort.prop }) (wfb₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := b₁, rty := LamSort.base LamBaseSort.prop }) (wfb₂ : LamWF lval.toLamTyVal { lctx := lctx, rterm := b₂, rty := LamSort.base LamBaseSort.prop }) : LamValid lval lctx ((a₁.mkImp a₂).mkImp ((b₁.mkImp b₂).mkImp ((a₁.mkAnd b₁).mkImp (a₂.mkAnd b₂))))

theorem Auto.Embedding.Lam.LamValid.and_imp_and_of_left_imp {lctx : Nat → LamSort} {a₁ a₂ b : LamTerm} {lval : LamValuation} (wfa₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := a₁, rty := LamSort.base LamBaseSort.prop }) (wfa₂ : LamWF lval.toLamTyVal { lctx := lctx, rterm := a₂, rty := LamSort.base LamBaseSort.prop }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.prop }) : LamValid lval lctx ((a₁.mkImp a₂).mkImp ((a₁.mkAnd b).mkImp (a₂.mkAnd b)))

theorem Auto.Embedding.Lam.LamValid.and_imp_and_of_right_imp {lctx : Nat → LamSort} {a b₁ b₂ : LamTerm} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.prop }) (wfb₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := b₁, rty := LamSort.base LamBaseSort.prop }) (wfb₂ : LamWF lval.toLamTyVal { lctx := lctx, rterm := b₂, rty := LamSort.base LamBaseSort.prop }) : LamValid lval lctx ((b₁.mkImp b₂).mkImp ((a.mkAnd b₁).mkImp (a.mkAnd b₂)))

theorem Auto.Embedding.Lam.LamValid.and_equiv {lval : LamValuation} {lctx : Nat → LamSort} {a b : LamTerm} : LamValid lval lctx (a.mkAnd b) ↔ LamValid lval lctx a ∧ LamValid lval lctx b

theorem Auto.Embedding.Lam.LamValid.and_left {lctx : Nat → LamSort} {a b : LamTerm} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.prop }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.prop }) : LamValid lval lctx ((a.mkAnd b).mkImp a)

theorem Auto.Embedding.Lam.LamValid.and_right {lctx : Nat → LamSort} {a b : LamTerm} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.prop }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.prop }) : LamValid lval lctx ((a.mkAnd b).mkImp b)

theorem Auto.Embedding.Lam.LamValid.or_imp_or_of_imp_imp {lctx : Nat → LamSort} {a₁ a₂ b₁ b₂ : LamTerm} {lval : LamValuation} (wfa₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := a₁, rty := LamSort.base LamBaseSort.prop }) (wfa₂ : LamWF lval.toLamTyVal { lctx := lctx, rterm := a₂, rty := LamSort.base LamBaseSort.prop }) (wfb₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := b₁, rty := LamSort.base LamBaseSort.prop }) (wfb₂ : LamWF lval.toLamTyVal { lctx := lctx, rterm := b₂, rty := LamSort.base LamBaseSort.prop }) : LamValid lval lctx ((a₁.mkImp a₂).mkImp ((b₁.mkImp b₂).mkImp ((a₁.mkOr b₁).mkImp (a₂.mkOr b₂))))

theorem Auto.Embedding.Lam.LamValid.or_imp_or_of_left_imp {lctx : Nat → LamSort} {a₁ a₂ b : LamTerm} {lval : LamValuation} (wfa₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := a₁, rty := LamSort.base LamBaseSort.prop }) (wfa₂ : LamWF lval.toLamTyVal { lctx := lctx, rterm := a₂, rty := LamSort.base LamBaseSort.prop }) (wfb : LamWF lval.toLamTyVal { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.prop }) : LamValid lval lctx ((a₁.mkImp a₂).mkImp ((a₁.mkOr b).mkImp (a₂.mkOr b)))

theorem Auto.Embedding.Lam.LamValid.or_imp_or_of_right_imp {lctx : Nat → LamSort} {a b₁ b₂ : LamTerm} {lval : LamValuation} (wfa : LamWF lval.toLamTyVal { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.prop }) (wfb₁ : LamWF lval.toLamTyVal { lctx := lctx, rterm := b₁, rty := LamSort.base LamBaseSort.prop }) (wfb₂ : LamWF lval.toLamTyVal { lctx := lctx, rterm := b₂, rty := LamSort.base LamBaseSort.prop }) : LamValid lval lctx ((b₁.mkImp b₂).mkImp ((a.mkOr b₁).mkImp (a.mkOr b₂)))

theorem Auto.Embedding.Lam.LamTerm.evarBounded_of_evarEquiv {f : LamTerm → Option LamTerm} {bound : Nat} (H : evarEquiv f) : evarBounded f bound

theorem Auto.Embedding.Lam.LamTerm.evarBounded_le {f : LamTerm → Option LamTerm} {bound bound' : Nat} (H : evarBounded f bound) (hle : bound ≤ bound') : evarBounded f bound'

theorem Auto.Embedding.Lam.LamTerm.evarBounded_none {bound : Nat} : evarBounded (fun (x : LamTerm) => none) bound

theorem Auto.Embedding.Lam.LamTerm.evarBounded_eqNone {f : LamTerm → Option LamTerm} {bound : Nat} (H : ∀ (t : LamTerm), f t = none) : evarBounded f bound

theorem Auto.Embedding.Lam.LamTerm.evarEquiv_none : evarEquiv fun (x : LamTerm) => none

theorem Auto.Embedding.Lam.LamTerm.evarEquiv_eqNone {f : LamTerm → Option LamTerm} (H : ∀ (t : LamTerm), f t = none) : evarEquiv f

theorem Auto.Embedding.Lam.LamTerm.evarBounded_rwGenAt {conv : LamTerm → Option LamTerm} {bound : Nat} {occ : List Bool} (H : evarBounded conv bound) : evarBounded (rwGenAt occ conv) bound

theorem Auto.Embedding.Lam.LamTerm.evarEquiv_rwGenAt {conv : LamTerm → Option LamTerm} {occ : List Bool} (H : evarEquiv conv) : evarEquiv (rwGenAt occ conv)

theorem Auto.Embedding.Lam.LamGenConv.none {lval : LamValuation} : LamGenConv lval fun (x : LamTerm) => Option.none

theorem Auto.Embedding.Lam.LamGenConv.eqNone {f : LamTerm → Option LamTerm} {lval : LamValuation} (H : ∀ (t : LamTerm), f t = Option.none) : LamGenConv lval f

theorem Auto.Embedding.Lam.LamGenConv.rwGenAt {lval : LamValuation} {conv : LamTerm → Option LamTerm} {occ : List Bool} (H : LamGenConv lval conv) : LamGenConv lval (LamTerm.rwGenAt occ conv)

theorem Auto.Embedding.Lam.LamTerm.evarBounded_rwGenAll {conv : LamTerm → Option LamTerm} {bound : Nat} (H : evarBounded conv bound) : evarBounded (rwGenAll conv) bound

theorem Auto.Embedding.Lam.LamTerm.evarEquiv_rwGenAll {conv : LamTerm → Option LamTerm} (H : evarEquiv conv) : evarEquiv (rwGenAll conv)

theorem Auto.Embedding.Lam.LamGenConv.rwGenAll {lval : LamValuation} {conv : LamTerm → Option LamTerm} (H : LamGenConv lval conv) : LamGenConv lval (LamTerm.rwGenAll conv)

theorem Auto.Embedding.Lam.LamTerm.evarBounded_rwGenAtWith {conv : LamSort → LamTerm → Option LamTerm} {bound : Nat} {occ : List Bool} (H : ∀ (s : LamSort), evarBounded (conv s) bound) (s : LamSort) : evarBounded (rwGenAtWith occ conv s) bound

theorem Auto.Embedding.Lam.LamTerm.evarEquiv_rwGenAtWith {conv : LamSort → LamTerm → Option LamTerm} {occ : List Bool} (H : ∀ (s : LamSort), evarEquiv (conv s)) (s : LamSort) : evarEquiv (rwGenAtWith occ conv s)

theorem Auto.Embedding.Lam.LamGenConvWith.none {lval : LamValuation} : LamGenConvWith lval fun (x : LamSort) (x : LamTerm) => Option.none

theorem Auto.Embedding.Lam.LamGenConvWith.eqNone {f : LamSort → LamTerm → Option LamTerm} {lval : LamValuation} (H : ∀ (s : LamSort) (t : LamTerm), f s t = Option.none) : LamGenConvWith lval f

theorem Auto.Embedding.Lam.LamGenConvWith.rwGenAtWith {lval : LamValuation} {conv : LamSort → LamTerm → Option LamTerm} {occ : List Bool} (H : LamGenConvWith lval conv) : LamGenConvWith lval (LamTerm.rwGenAtWith occ conv)

theorem Auto.Embedding.Lam.LamTerm.evarBounded_rwGenAllWith {conv : LamSort → LamTerm → Option LamTerm} {bound : Nat} (H : ∀ (s : LamSort), evarBounded (conv s) bound) (s : LamSort) : evarBounded (rwGenAllWith conv s) bound

theorem Auto.Embedding.Lam.LamTerm.evarEquiv_rwGenAllWith {conv : LamSort → LamTerm → Option LamTerm} (H : ∀ (s : LamSort), evarEquiv (conv s)) (s : LamSort) : evarEquiv (rwGenAllWith conv s)

theorem Auto.Embedding.Lam.LamGenConvWith.rwGenAllWith {lval : LamValuation} {conv : LamSort → LamTerm → Option LamTerm} (H : LamGenConvWith lval conv) : LamGenConvWith lval (LamTerm.rwGenAllWith conv)

theorem Auto.Embedding.Lam.LamTerm.evarEquiv_rwGenAtIfSign {b : Bool} {occ : List Bool} {modify : LamTerm → Option LamTerm} (H : evarEquiv modify) : evarEquiv (rwGenAtIfSign b occ modify)

theorem Auto.Embedding.Lam.LamTerm.evarBounded_rwGenAtIfSign {n : Nat} {b : Bool} {occ : List Bool} {modify : LamTerm → Option LamTerm} (H : evarBounded modify n) : evarBounded (rwGenAtIfSign b occ modify) n

theorem Auto.Embedding.Lam.LamGenModify.rwGenAtIfSign {lval : LamValuation} {weaken? weaken?' : Bool} {occ : List Bool} {modify : LamTerm → Option LamTerm} (H : LamGenModify lval modify weaken?) : LamGenModify lval (LamTerm.rwGenAtIfSign (weaken? == weaken?') occ modify) weaken?'

def Auto.Embedding.Lam.LamTerm.emb : LamTerm

Equations

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

def Auto.Embedding.Lam.LamWF.emb {ltv : LamTyVal} {lctx : Nat → LamSort} : LamWF ltv { lctx := lctx, rterm := LamTerm.emb, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamThmValid.emb {lval : LamValuation} : LamThmValid lval [] LamTerm.emb

def Auto.Embedding.Lam.LamTerm.false_ne_true : LamTerm

Equations

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

def Auto.Embedding.Lam.LamWF.false_ne_true {ltv : LamTyVal} {lctx : Nat → LamSort} : LamWF ltv { lctx := lctx, rterm := LamTerm.false_ne_true, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamThmValid.false_ne_true {lval : LamValuation} : LamThmValid lval [] LamTerm.false_ne_true

def Auto.Embedding.Lam.LamTerm.not_true_eq_false : LamTerm

Equations

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

def Auto.Embedding.Lam.LamWF.not_true_eq_false {ltv : LamTyVal} {lctx : Nat → LamSort} : LamWF ltv { lctx := lctx, rterm := LamTerm.not_true_eq_false, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamThmValid.not_true_eq_false {lval : LamValuation} : LamThmValid lval [] LamTerm.not_true_eq_false

def Auto.Embedding.Lam.LamTerm.not_false_eq_true : LamTerm

Equations

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

def Auto.Embedding.Lam.LamWF.not_false_eq_true {ltv : LamTyVal} {lctx : Nat → LamSort} : LamWF ltv { lctx := lctx, rterm := LamTerm.not_false_eq_true, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamThmValid.not_false_eq_true {lval : LamValuation} : LamThmValid lval [] LamTerm.not_false_eq_true

def Auto.Embedding.Lam.LamTerm.false_and_eq_false : LamTerm

Equations

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

def Auto.Embedding.Lam.LamWF.false_and_eq_false {ltv : LamTyVal} {lctx : Nat → LamSort} : LamWF ltv { lctx := lctx, rterm := LamTerm.false_and_eq_false, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamThmValid.false_and_eq_false {lval : LamValuation} : LamThmValid lval [] LamTerm.false_and_eq_false

def Auto.Embedding.Lam.LamTerm.true_and_eq_id : LamTerm

Equations

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

def Auto.Embedding.Lam.LamWF.true_and_eq_id {ltv : LamTyVal} {lctx : Nat → LamSort} : LamWF ltv { lctx := lctx, rterm := LamTerm.true_and_eq_id, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamThmValid.true_and_eq_id {lval : LamValuation} : LamThmValid lval [] LamTerm.true_and_eq_id

def Auto.Embedding.Lam.LamTerm.false_or_eq_id : LamTerm

Equations

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

def Auto.Embedding.Lam.LamWF.false_or_eq_id {ltv : LamTyVal} {lctx : Nat → LamSort} : LamWF ltv { lctx := lctx, rterm := LamTerm.false_or_eq_id, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamThmValid.false_or_eq_id {lval : LamValuation} : LamThmValid lval [] LamTerm.false_or_eq_id

def Auto.Embedding.Lam.LamTerm.true_or_eq_true : LamTerm

Equations

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

def Auto.Embedding.Lam.LamWF.true_or_eq_true {ltv : LamTyVal} {lctx : Nat → LamSort} : LamWF ltv { lctx := lctx, rterm := LamTerm.true_or_eq_true, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamThmValid.true_or_eq_true {lval : LamValuation} : LamThmValid lval [] LamTerm.true_or_eq_true

def Auto.Embedding.Lam.LamTerm.ofPropSpec : LamTerm

Equations

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

def Auto.Embedding.Lam.LamWF.ofPropSpec {ltv : LamTyVal} {lctx : Nat → LamSort} : LamWF ltv { lctx := lctx, rterm := LamTerm.ofPropSpec, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamThmValid.ofPropSpec {lval : LamValuation} : LamThmValid lval [] LamTerm.ofPropSpec

def Auto.Embedding.Lam.LamTerm.boolFacts : LamTerm

Equations

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

def Auto.Embedding.Lam.LamWF.boolFacts {ltv : LamTyVal} {lctx : Nat → LamSort} : LamWF ltv { lctx := lctx, rterm := LamTerm.boolFacts, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_boolFacts : boolFacts.maxEVarSucc = 0

theorem Auto.Embedding.Lam.LamThmValid.boolFacts {lval : LamValuation} : LamThmValid lval [] LamTerm.boolFacts

def Auto.Embedding.Lam.LamTerm.iteSpec (s : LamSort) : LamTerm

Equations

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

def Auto.Embedding.Lam.LamWF.iteSpec {ltv : LamTyVal} {lctx : Nat → LamSort} (s : LamSort) : LamWF ltv { lctx := lctx, rterm := LamTerm.iteSpec s, rty := LamSort.base LamBaseSort.prop }

Equations

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

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_iteSpec (s : LamSort) : (iteSpec s).maxEVarSucc = 0

theorem Auto.Embedding.Lam.LamThmValid.iteSpec {lval : LamValuation} (s : LamSort) : LamThmValid lval [] (LamTerm.iteSpec s)