---

Step * 1 2 of Lemma mFOL-evidence-value-type


1. isall : 𝔹
2. var : ℤ
3. f3 : mFOL()
4. value-type(mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅))
5. ↑isall
⊢ ∃v:Unit. value-type(mFOL-abstract(f3) Unit (λn,L. True) λz.⋅[var := v])
BY
{ xxx(With ⌜⋅⌝ (D 0)⋅ THEN Auto)xxx }

1
1. isall : 𝔹
2. var : ℤ
3. f3 : mFOL()
4. value-type(mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅))
5. ↑isall
⊢ value-type(mFOL-abstract(f3) Unit (λn,L. True) λz.⋅[var := ⋅])

---

Latex:

---

Latex:

1.  isall  :  \mBbbB{}
2.  var  :  \mBbbZ{}
3.  f3  :  mFOL()
4.  value-type(mFOL-abstract(f3)  Unit  (\mlambda{}n,L.  True)  (\mlambda{}z.\mcdot{}))
5.  \muparrow{}isall
\mvdash{}  \mexists{}v:Unit.  value-type(mFOL-abstract(f3)  Unit  (\mlambda{}n,L.  True)  \mlambda{}z.\mcdot{}[var  :=  v])


By

---

Latex:
xxx(With  \mkleeneopen{}\mcdot{}\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)xxx

---

Home Index