---

Step * 2 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)
4. n : node
⊢ (∀f1∈fst(n).(∀f∈localT prop(f1).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.  \mforall{}n:node.  (\mforall{}f\mmember{}fst(n).f  \mmember{}  Prop)
4.  n  :  node
\mvdash{}  (\mforall{}f1\mmember{}fst(n).(\mforall{}f\mmember{}localT  prop(f1).f  \mmember{}  Prop))


By

---

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

---

Home Index