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

Equations

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

theorem Auto.Embedding.Lam.LamTerm.evarBounded_andLeft? : evarBounded andLeft? 0

theorem Auto.Embedding.Lam.LamGenModify.andLeft? {lval : LamValuation} : LamGenModify lval LamTerm.andLeft? true

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

Equations

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

theorem Auto.Embedding.Lam.LamTerm.evarBounded_andRight? : evarBounded andRight? 0

theorem Auto.Embedding.Lam.LamGenModify.andRight? {lval : LamValuation} : LamGenModify lval LamTerm.andRight? true

theorem Auto.Embedding.Lam.eq_not_of_ne {a b : Prop} (h : a ≠ b) : a = ¬b

theorem Auto.Embedding.Lam.ne_of_eq_not {a b : Prop} (h : a = ¬b) : a ≠ b

theorem Auto.Embedding.Lam.equiv_eq {a b : Prop} : (a ↔ b) = (a = b)

theorem Auto.Embedding.Lam.not_equiv_eq {a b : Prop} : (¬(a ↔ b)) = (a ≠ b)

theorem Auto.Embedding.Lam.propeq_equiv {a b : Prop} : a = b ↔ (a ∨ ¬b) ∧ (¬a ∨ b)

theorem Auto.Embedding.Lam.propne_equiv {a b : Prop} : a ≠ b ↔ (a ∨ b) ∧ (¬a ∨ ¬b)

theorem Auto.Embedding.Lam.LamEquiv.not_true_equiv_false {lval : LamValuation} {lctx : Nat → LamSort} : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (LamTerm.base LamBaseTerm.trueE).mkNot (LamTerm.base LamBaseTerm.falseE)

theorem Auto.Embedding.Lam.LamEquiv.not_false_equiv_true {lval : LamValuation} {lctx : Nat → LamSort} : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (LamTerm.base LamBaseTerm.falseE).mkNot (LamTerm.base LamBaseTerm.trueE)

theorem Auto.Embedding.Lam.LamEquiv.prop_ne_equiv_eq_not {lctx : Nat → LamSort} {lhs rhs : LamTerm} {lval : LamValuation} (wfl : LamWF lval.toLamTyVal { lctx := lctx, rterm := lhs, rty := LamSort.base LamBaseSort.prop }) (wfr : LamWF lval.toLamTyVal { lctx := lctx, rterm := rhs, rty := LamSort.base LamBaseSort.prop }) : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) (LamTerm.mkEq (LamSort.base LamBaseSort.prop) lhs rhs).mkNot (LamTerm.mkEq (LamSort.base LamBaseSort.prop) lhs rhs.mkNot)

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

(a ≠ b) ↔ (a = (¬ b))

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.prop_ne_equiv_eq_not? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.prop_ne_equiv_eq_not? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.prop_ne_equiv_eq_not? {lval : LamValuation} : LamGenConv lval LamTerm.prop_ne_equiv_eq_not?

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

Equations

• t.equalize = Auto.Embedding.Lam.LamTerm.mkEq (Auto.Embedding.Lam.LamSort.base Auto.Embedding.Lam.LamBaseSort.prop) t (Auto.Embedding.Lam.LamTerm.base Auto.Embedding.Lam.LamBaseTerm.trueE)

theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_equalize {t : LamTerm} : t.equalize.maxEVarSucc = t.maxEVarSucc

theorem Auto.Embedding.Lam.LamEquiv.equalize {lctx : Nat → LamSort} {t : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := LamSort.base LamBaseSort.prop }) : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t.equalize

def Auto.Embedding.Lam.LamTerm.equalize? (s : LamSort) (t : LamTerm) : Option LamTerm

Equations

• One or more equations did not get rendered due to their size.
• Auto.Embedding.Lam.LamTerm.equalize? s t = none

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

theorem Auto.Embedding.Lam.LamEquiv.equalize? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := LamSort.base LamBaseSort.prop }) (heq : LamTerm.equalize? s t = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.equalize? {lval : LamValuation} : LamGenConvWith lval LamTerm.equalize?

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

(True = False) ↔ False

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.true_eq_false_equiv_false? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.true_eq_false_equiv_false? = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.true_eq_false_equiv_false? {lval : LamValuation} : LamGenConv lval LamTerm.true_eq_false_equiv_false?

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

(False = True) ↔ False

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.false_eq_true_equiv_false? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.false_eq_true_equiv_false? = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.false_eq_true_equiv_false? {lval : LamValuation} : LamGenConv lval LamTerm.false_eq_true_equiv_false?

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

(a = True) ↔ a

At first sight, it seems that this theorem will never be used in clausification. However, it will, as we need to turn (a = b) = True into a = b

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.eq_true_equiv? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.eq_true_equiv? = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.eq_true_equiv? {lval : LamValuation} : LamGenConv lval LamTerm.eq_true_equiv?

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

(a = False) ↔ (¬ a)

At first sight, it seems that this theorem will never be used in clausification. However, it will, as we need to turn (a = b) = False into a ≠ b

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.eq_false_equiv? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.eq_false_equiv? = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.eq_false_equiv? {lval : LamValuation} : LamGenConv lval LamTerm.eq_false_equiv?

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

(a ≠ True) ↔ (a = False)

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.ne_true_equiv_eq_false? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.ne_true_equiv_eq_false? = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.ne_true_equiv_eq_false? {lval : LamValuation} : LamGenConv lval LamTerm.ne_true_equiv_eq_false?

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

(a ≠ False) ↔ (a = True)

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.ne_false_equiv_eq_true? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.ne_false_equiv_eq_true? = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.ne_false_equiv_eq_true? {lval : LamValuation} : LamGenConv lval LamTerm.ne_false_equiv_eq_true?

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

((¬ a) = True) ↔ (a = False)

Equations

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

def Auto.Embedding.Lam.LamTerm.maxEVarSucc_not_eq_true_equiv_eq_false? {t t' : LamTerm} (heq : t.not_eq_true_equiv_eq_false? = some t') : t'.maxEVarSucc = t.maxEVarSucc

Equations

• ⋯ = ⋯

theorem Auto.Embedding.Lam.LamEquiv.not_eq_true_equiv_eq_false? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.not_eq_true_equiv_eq_false? = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.not_eq_true_equiv_eq_false? {lval : LamValuation} : LamGenConv lval LamTerm.not_eq_true_equiv_eq_false?

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

((¬ a) = False) ↔ (a = True)

Equations

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

def Auto.Embedding.Lam.LamTerm.maxEVarSucc_not_eq_false_equiv_eq_true? {t t' : LamTerm} (heq : t.not_eq_false_equiv_eq_true? = some t') : t'.maxEVarSucc = t.maxEVarSucc

Equations

• ⋯ = ⋯

theorem Auto.Embedding.Lam.LamEquiv.not_eq_false_equiv_eq_true? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.not_eq_false_equiv_eq_true? = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.not_eq_false_equiv_eq_true? {lval : LamValuation} : LamGenConv lval LamTerm.not_eq_false_equiv_eq_true?

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

(¬¬a) ↔ a

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

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.not_not_equiv? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.not_not_equiv? = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.not_not_equiv? {lval : LamValuation} : LamGenConv lval LamTerm.not_not_equiv?

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

((¬ a) = b) ↔ (a = (¬ b))

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.not_eq_equiv_eq_not? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.not_eq_equiv_eq_not? = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.not_eq_equiv_eq_not? {lval : LamValuation} : LamGenConv lval LamTerm.not_eq_equiv_eq_not?

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

((¬ a) = (¬ b)) ↔ (a = b)

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.not_eq_not_equiv_eq? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.not_eq_not_equiv_eq? = some t') : s = LamSort.base LamBaseSort.prop ∧ LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.not_eq_not_equiv_eq? {lval : LamValuation} : LamGenConv lval LamTerm.not_eq_not_equiv_eq?

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

(a ↔ b) ↔ (a = b)

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.propext? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.propext? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.propext? {lval : LamValuation} : LamGenConv lval LamTerm.propext?

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

¬ (a ∧ b) ↔ ¬ a ∨ ¬ b

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.not_and_equiv_not_or_not? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.not_and_equiv_not_or_not? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.not_and_equiv_not_or_not? {lval : LamValuation} : LamGenConv lval LamTerm.not_and_equiv_not_or_not?

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

¬ (a ∨ b) ↔ ¬ a ∧ ¬ b

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.not_or_equiv_not_and_not? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.not_or_equiv_not_and_not? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.not_or_equiv_not_and_not? {lval : LamValuation} : LamGenConv lval LamTerm.not_or_equiv_not_and_not?

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

(a = b) ↔ (a ∨ ¬ b) ∧ (¬ a ∨ b)

Equations

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

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

theorem Auto.Embedding.Lam.propeq_equiv_eq' {a b : GLift Prop} : a = b ↔ (a.down ∨ ¬b.down) ∧ (¬a.down ∨ b.down)

theorem Auto.Embedding.Lam.LamEquiv.propeq? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.propeq? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.propeq? {lval : LamValuation} : LamGenConv lval LamTerm.propeq?

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

(a → b) ↔ (¬ a ∨ b)

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.imp_equiv_not_or? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.imp_equiv_not_or? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.imp_equiv_not_or? {lval : LamValuation} : LamGenConv lval LamTerm.imp_equiv_not_or?

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

(¬ (a → b)) ↔ (a ∧ ¬ b)

Equations

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

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

theorem Auto.Embedding.Lam.LamEquiv.not_imp_equiv_and_not? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.not_imp_equiv_and_not? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.not_imp_equiv_and_not? {lval : LamValuation} : LamGenConv lval LamTerm.not_imp_equiv_and_not?

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

(a = b) ↔ (a ∨ b) ∧ (¬ a ∨ ¬ b)

Equations

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

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

theorem Auto.Embedding.Lam.propne_equiv_eq' {a b : GLift Prop} : a ≠ b ↔ (a.down ∨ b.down) ∧ (¬a.down ∨ ¬b.down)

theorem Auto.Embedding.Lam.LamEquiv.propne? {lctx : Nat → LamSort} {t : LamTerm} {s : LamSort} {t' : LamTerm} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := s }) (heq : t.propne? = some t') : LamEquiv lval lctx (LamSort.base LamBaseSort.prop) t t'

theorem Auto.Embedding.Lam.LamGenConv.propne? {lval : LamValuation} : LamGenConv lval LamTerm.propne?