---

Step * of Lemma evalall-append-implies-rec-value

∀[a,b:Base].  b ∈ rec-value() supposing (evalall(a @ b))↓
BY
{ (Auto
   THEN (FLemma `evalall-append-implies-list` [-1] THENA Auto)
   THEN MoveToConcl (-2)
   THEN GenConclAtAddr [1;1;1;1]
   THEN ThinVar `a') }

1
1. b : Base
2. v : rec-value() List
⊢ (evalall(v @ b))↓ ⇒ (b ∈ rec-value())

---

Latex:

---

Latex:
\mforall{}[a,b:Base].    b  \mmember{}  rec-value()  supposing  (evalall(a  @  b))\mdownarrow{}


By

---

Latex:
(Auto
  THEN  (FLemma  `evalall-append-implies-list`  [-1]  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  GenConclAtAddr  [1;1;1;1]
  THEN  ThinVar  `a')

---

Home Index