---

Step * 1 2 1 1 1 13 of Lemma mFOL-proveable-evidence


1. hyps : mFOL() List
2. concl : mFOL()
3. subgoals : mFOL-sequent() List
4. ∀i:ℕ||subgoals||. mFOL-sequent-evidence(subgoals[i])
5. hypnum : ℕ
6. (inr ⋅ ) = (inl subgoals) ∈ (mFOL-sequent() List?)
7. mFOL-sequent-evidence(subgoals[0])
8. mFOL-sequent-evidence(subgoals[1])
⊢ mFOL-sequent-evidence(<hyps, concl>)
BY
{ Auto }

---

Latex:

---

Latex:

1.  hyps  :  mFOL()  List
2.  concl  :  mFOL()
3.  subgoals  :  mFOL-sequent()  List
4.  \mforall{}i:\mBbbN{}||subgoals||.  mFOL-sequent-evidence(subgoals[i])
5.  hypnum  :  \mBbbN{}
6.  (inr  \mcdot{}  )  =  (inl  subgoals)
7.  mFOL-sequent-evidence(subgoals[0])
8.  mFOL-sequent-evidence(subgoals[1])
\mvdash{}  mFOL-sequent-evidence(<hyps,  concl>)


By

---

Latex:
Auto

---

Home Index