---

Step * of Lemma coW-wfdd_functionality

∀[A:𝕌']. ∀B:A ⟶ Type. ∀w,w':coW(A;a.B[a]).  (coW-equiv(a.B[a];w;w') ⇒ (coW-wfdd(a.B[a];w) ⇐⇒ coW-wfdd(a.B[a];w')))
BY
{ (RepeatFor 2 (Intro)
   THEN Assert ⌜∀w,w':coW(A;a.B[a]).  (coW-equiv(a.B[a];w;w') ⇒ coW-wfdd(a.B[a];w) ⇒ coW-wfdd(a.B[a];w'))⌝⋅
   ) }

1
.....assertion..... 
1. [A] : 𝕌'
2. B : A ⟶ Type
⊢ ∀w,w':coW(A;a.B[a]).  (coW-equiv(a.B[a];w;w') ⇒ coW-wfdd(a.B[a];w) ⇒ coW-wfdd(a.B[a];w'))

2
1. [A] : 𝕌'
2. B : A ⟶ Type
3. ∀w,w':coW(A;a.B[a]).  (coW-equiv(a.B[a];w;w') ⇒ coW-wfdd(a.B[a];w) ⇒ coW-wfdd(a.B[a];w'))
⊢ ∀w,w':coW(A;a.B[a]).  (coW-equiv(a.B[a];w;w') ⇒ (coW-wfdd(a.B[a];w) ⇐⇒ coW-wfdd(a.B[a];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')  {}\mRightarrow{}  (coW-wfdd(a.B[a];w)  \mLeftarrow{}{}\mRightarrow{}  coW-wfdd(a.B[a];w')))


By

---

Latex:
(RepeatFor  2  (Intro)
  THEN  Assert  \mkleeneopen{}\mforall{}w,w':coW(A;a.B[a]).
                                (coW-equiv(a.B[a];w;w')  {}\mRightarrow{}  coW-wfdd(a.B[a];w)  {}\mRightarrow{}  coW-wfdd(a.B[a];w'))\mkleeneclose{}\mcdot{}
  )

---

Home Index