---

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


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

---

Latex:

---

Latex:

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


By

---

Latex:
Obvious

---

Home Index