---

Step * 3 2 1 1 2 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
6. u : A × B@i
7. v : (A × B) List@i
8. b : B@i
9. (fst(u)) = a ∈ A
10. b = (snd(u)) ∈ B@i
⊢ <a, b> = u ∈ (A × B)
BY
{ (DVar `u' THEN All Reduce THEN EqCD THEN Auto)⋅ }

---

Latex:



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


By

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

---

Home Index