---

Step * 1 3 1 1 1 1 of Lemma FOL-sequent-evidence-false-hyp


1. v : mFOL()
⊢ (↑mFOatomic?(v))
⇒ (mFOatomic-name(v) = "false" ∈ Atom)
⇒ (mFOatomic-vars(v) = [] ∈ (ℤ List))
⇒ (v = false ∈ mFOL())
BY
{ (MoveToConcl(-1) THEN (BLemma `mFOL-induction` THENA Auto) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  v  :  mFOL()
\mvdash{}  (\muparrow{}mFOatomic?(v))  {}\mRightarrow{}  (mFOatomic-name(v)  =  "false")  {}\mRightarrow{}  (mFOatomic-vars(v)  =  [])  {}\mRightarrow{}  (v  =  false)


By

---

Latex:
(MoveToConcl(-1)  THEN  (BLemma  `mFOL-induction`  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index