---

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


1. A : Type
2. B : Type
3. eq1 : EqDecider(A)
4. eq2 : EqDecider(B)
5. a : A
6. u : A × B
7. v : (A × B) List
8. b : B
9. (fst(u)) = a ∈ A
10. b = (snd(u)) ∈ B
⊢ <a, b> = u ∈ (A × B)
BY
{ (DVar `u' THEN All Reduce THEN EqCD THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  eq1  :  EqDecider(A)
4.  eq2  :  EqDecider(B)
5.  a  :  A
6.  u  :  A  \mtimes{}  B
7.  v  :  (A  \mtimes{}  B)  List
8.  b  :  B
9.  (fst(u))  =  a
10.  b  =  (snd(u))
\mvdash{}  <a,  b>  =  u


By

---

Latex:
(DVar  `u'  THEN  All  Reduce  THEN  EqCD  THEN  Auto)\mcdot{}

---

Home Index