---

Step * 3 2 1 1 1 of Lemma pairs-fpf_property


1. [A] : Type
2. [B] : Type
3. eq1 : EqDecider(A)@i
4. eq2 : EqDecider(B)@i
5. a : A@i
⊢ ∀b:B. ((b ∈ []) ⇐⇒ (<a, b> ∈ []))
BY
{ Obvious }

---

Latex:



1.  [A]  :  Type
2.  [B]  :  Type
3.  eq1  :  EqDecider(A)@i
4.  eq2  :  EqDecider(B)@i
5.  a  :  A@i
\mvdash{}  \mforall{}b:B.  ((b  \mmember{}  [])  \mLeftarrow{}{}\mRightarrow{}  (<a,  b>  \mmember{}  []))


By

Obvious

---

Home Index