---

Step * 3 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))
5. n : node
⊢ (∀f∈fst(n).(∀f1∈localT prop(f).(∃f1'∈fst(n). dlo_eq(prop(f1);prop(f1')) ∈ 𝔹)))
BY
{ ((Unfold `l_all` 0 THEN Auto) THEN Unfold `l_exists` 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.  \mforall{}n:node.  (\mforall{}f1\mmember{}fst(n).(\mforall{}f\mmember{}localT  prop(f1).f  \mmember{}  Prop))
5.  n  :  node
\mvdash{}  (\mforall{}f\mmember{}fst(n).(\mforall{}f1\mmember{}localT  prop(f).(\mexists{}f1'\mmember{}fst(n).  dlo\_eq(prop(f1);prop(f1'))  \mmember{}  \mBbbB{})))


By

---

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

---

Home Index