---

Step * of Lemma mFOL-sequent-evidence-trivial

∀hyps:mFOL() List. ∀i:ℕ||hyps||.  mFOL-sequent-evidence(<hyps, hyps[i]>)
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN RepUR ``mFOL-sequent-abstract FOSatWith`` 0
   THEN Fold `FOSatWith` 0
   THEN UseWitness ⌈λx.x.i⌉⋅
   THEN Auto
   THEN DVar `i'
   THEN Auto
   THEN (DoSubsume⋅ THEN Auto THEN (RWO "select-map" 0 THEN Auto) THEN Reduce 0 THEN Auto)⋅) }

---

Latex:


\mforall{}hyps:mFOL()  List.  \mforall{}i:\mBbbN{}||hyps||.    mFOL-sequent-evidence(<hyps,  hyps[i]>)


By

(Auto
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``mFOL-sequent-abstract  FOSatWith``  0
  THEN  Fold  `FOSatWith`  0
  THEN  UseWitness  \mkleeneopen{}\mlambda{}x.x.i\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  DVar  `i'
  THEN  Auto
  THEN  (DoSubsume\mcdot{}  THEN  Auto  THEN  (RWO  "select-map"  0  THEN  Auto)  THEN  Reduce  0  THEN  Auto)\mcdot{})

---

Home Index