---

Step * of Lemma mFOL-sequent-evidence_and

∀hyps:mFOL() List. ∀[x,y:mFOL()].  (mFOL-sequent-evidence(<hyps, x>) ⇒ mFOL-sequent-evidence(<hyps, y>) ⇒ mFOL-sequent\000C-evidence(<hyps, x ∧ y>))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN ((Assert Dom,S,a |= mFOL-sequent-abstract(<hyps, x>) ∧ Dom,S,a |= mFOL-sequent-abstract(<hyps, y>) BY
                (Auto
                 THEN All (RepUR ``mFOL-sequent-evidence mFO-uniform-evidence``)
                 THEN BackThruSomeHyp
                 THEN (DoSubsume THEN Auto)
                 THEN SubtypeReasoning1
                 THEN Auto
                 THEN BLemma_o (ioid Obid: mFOL-sequent-freevars-subset-3)⋅
                 THEN Auto
                 THEN RepUR ``mFOL-freevars`` 0
                 THEN Fold `mFOL-freevars` 0
                 THEN RWO "val-union-l-union" 0
                 THEN Auto))
         THEN (D -1
               THEN All (RepUR ``mFOL-sequent-abstract FOSatWith``)⋅
               THEN (All (Fold `implies`) THEN All (Fold `FOSatWith`))
               THEN Auto
               THEN ThinTrivial
               THEN (RepUR ``mFOL-abstract`` 0
                     THEN Fold `mFOL-abstract` 0
                     THEN RepUR ``FOConnective FOSatWith let`` 0
                     THEN All (Fold `FOSatWith`)
                     THEN Auto)⋅)
         )⋅) }

---

Latex:

---

Latex:
\mforall{}hyps:mFOL()  List.  \mforall{}[x,y:mFOL()].    (mFOL-sequent-evidence(<hyps,  x>)  {}\mRightarrow{}  mFOL-sequent-evidence(<hyps,\000C  y>)  {}\mRightarrow{}  mFOL-sequent-evidence(<hyps,  x  \mwedge{}  y>))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  ((Assert  Dom,S,a  |=  mFOL-sequent-abstract(<hyps,  x>)  \mwedge{}  Dom,S,a  |=  mFOL-sequent-abstract(<hyps,\000C  y>)  BY
                            (Auto
                              THEN  All  (RepUR  ``mFOL-sequent-evidence  mFO-uniform-evidence``)
                              THEN  BackThruSomeHyp
                              THEN  (DoSubsume  THEN  Auto)
                              THEN  SubtypeReasoning1
                              THEN  Auto
                              THEN  BLemma\_o  (ioid  Obid:  mFOL-sequent-freevars-subset-3)\mcdot{}
                              THEN  Auto
                              THEN  RepUR  ``mFOL-freevars``  0
                              THEN  Fold  `mFOL-freevars`  0
                              THEN  RWO  "val-union-l-union"  0
                              THEN  Auto))
              THEN  (D  -1
                          THEN  All  (RepUR  ``mFOL-sequent-abstract  FOSatWith``)\mcdot{}
                          THEN  (All  (Fold  `implies`)  THEN  All  (Fold  `FOSatWith`))
                          THEN  Auto
                          THEN  ThinTrivial
                          THEN  (RepUR  ``mFOL-abstract``  0
                                      THEN  Fold  `mFOL-abstract`  0
                                      THEN  RepUR  ``FOConnective  FOSatWith  let``  0
                                      THEN  All  (Fold  `FOSatWith`)
                                      THEN  Auto)\mcdot{})
              )\mcdot{})

---

Home Index