---

Step * of Lemma pi-trans_wf

∀[l_loc:Id]. ∀[P:pi_term()].  (pi-trans(l_loc;P) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process())
BY
{ (D 0 THENA Auto) }

1
1. l_loc : Id
⊢ ∀[P:pi_term()]. (pi-trans(l_loc;P) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process())

---

Latex:

---

Latex:
\mforall{}[l$_{loc}$:Id].  \mforall{}[P:pi\_term()].    (pi-trans(l$_{loc}$;P)  \mmember{}  I\000Cd  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process())


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index