---

Step * of Lemma mFOL-evidence-value-type

∀[fmla:mFOL()]. value-type(mFOL-evidence(fmla))
BY
{ ((D 0 THENA Auto)
   THEN RepUR ``mFOL-evidence mFO-uniform-evidence`` 0
   THEN Auto
   THEN With
   ⌈Unit⌉ (D 0)⋅
   THEN Auto
   THEN With ⌈λn,L. True⌉ (D 0)⋅
   THEN Auto
   THEN D 0
   THEN With ⌈λz.⋅⌉ (D 0)⋅
   THEN Auto
   THEN RepUR ``FOSatWith`` 0) }

1
1. fmla : mFOL()
⊢ value-type(mFOL-abstract(fmla) Unit (λn,L. True) (λz.⋅))

---

Latex:


\mforall{}[fmla:mFOL()].  value-type(mFOL-evidence(fmla))


By

((D  0  THENA  Auto)
  THEN  RepUR  ``mFOL-evidence  mFO-uniform-evidence``  0
  THEN  Auto
  THEN  With
  \mkleeneopen{}Unit\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  With  \mkleeneopen{}\mlambda{}n,L.  True\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  D  0
  THEN  With  \mkleeneopen{}\mlambda{}z.\mcdot{}\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  RepUR  ``FOSatWith``  0)

---

Home Index