---

Step * 1 of Lemma ncomplete-test


1. ∀a:Prop. (localT prop(a) ∈ Prop List)
2. ∀n:node. (fst(n) ∈ Prop List)
3. n : node
⊢ (∀f∈fst(n).f ∈ Prop)
BY
{ (Unfold `l_all` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}a:Prop.  (localT  prop(a)  \mmember{}  Prop  List)
2.  \mforall{}n:node.  (fst(n)  \mmember{}  Prop  List)
3.  n  :  node
\mvdash{}  (\mforall{}f\mmember{}fst(n).f  \mmember{}  Prop)


By

---

Latex:
(Unfold  `l\_all`  0  THEN  Auto)

---

Home Index