---

Step * of Lemma coW-equiv-iff

∀[A:𝕌']
  ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]).
    (coW-equiv(a.B[a];w;w') ⇐⇒ ∀z:coW(A;a.B[a]). (coWmem(a.B[a];z;w) ⇐⇒ coWmem(a.B[a];z;w')))
BY
{ (Intros THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. coW-equiv(a.B[a];w;w')
⊢ ∀z:coW(A;a.B[a]). (coWmem(a.B[a];z;w) ⇐⇒ coWmem(a.B[a];z;w'))

2
1. [A] : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. w' : coW(A;a.B[a])
5. ∀z:coW(A;a.B[a]). (coWmem(a.B[a];z;w) ⇐⇒ coWmem(a.B[a];z;w'))
⊢ coW-equiv(a.B[a];w;w')

---

Latex:

---

Latex:
\mforall{}[A:\mBbbU{}']
    \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}w,w':coW(A;a.B[a]).
        (coW-equiv(a.B[a];w;w')  \mLeftarrow{}{}\mRightarrow{}  \mforall{}z:coW(A;a.B[a]).  (coWmem(a.B[a];z;w)  \mLeftarrow{}{}\mRightarrow{}  coWmem(a.B[a];z;w')))


By

---

Latex:
(Intros  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index