---

Step * of Lemma norm-intransit_wf

∀[M:Type ⟶ Type]. ∀[intr:pInTransit(P.M[P])].
  (norm-intransit(intr) ∈ {intr':pInTransit(P.M[P])| intr' = intr ∈ pInTransit(P.M[P])} )
BY
{ (UnivCD THENA Auto) }

1
1. M : Type ⟶ Type
2. intr : pInTransit(P.M[P])
⊢ norm-intransit(intr) ∈ {intr':pInTransit(P.M[P])| intr' = intr ∈ pInTransit(P.M[P])} 

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[intr:pInTransit(P.M[P])].
    (norm-intransit(intr)  \mmember{}  \{intr':pInTransit(P.M[P])|  intr'  =  intr\}  )


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index