---

Step * of Lemma permr_suptyping

∀T:Type. ∀Q:T ⟶ ℙ. ∀as,bs:{z:T| Q[z]}  List.  ((as ≡(T) bs) ⇒ (as ≡({z:T| Q[z]} ) bs))
BY
{ (UnivCD THENA Auto) }

1
1. T : Type
2. Q : T ⟶ ℙ
3. as : {z:T| Q[z]}  List
4. bs : {z:T| Q[z]}  List
5. as ≡(T) bs
⊢ as ≡({z:T| Q[z]} ) bs

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  \mforall{}as,bs:\{z:T|  Q[z]\}    List.    ((as  \mequiv{}(T)  bs)  {}\mRightarrow{}  (as  \mequiv{}(\{z:T|  Q[z]\}  )  bs))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index