---

Step * 2 1 of Lemma pair-order


1. A : Type
2. B : Type
3. Ra : A ⟶ A ⟶ ℙ
4. Rb : B ⟶ B ⟶ ℙ
5. Refl(A;a,a'.Ra[a;a'])
6. Trans(A;a,a'.Ra[a;a'])
7. AntiSym(A;a,a'.Ra[a;a'])
8. Refl(B;b,b'.Rb[b;b'])
9. Trans(B;b,b'.Rb[b;b'])
10. AntiSym(B;b,b'.Rb[b;b'])
11. Refl(A × B;x,y.Ra[fst(x);fst(y)] ∧ ((¬((fst(x)) = (fst(y)) ∈ A)) ∨ Rb[snd(x);snd(y)]))
12. Trans(A × B;x,y.Ra[fst(x);fst(y)] ∧ ((¬((fst(x)) = (fst(y)) ∈ A)) ∨ Rb[snd(x);snd(y)]))
13. x : A × B
14. y : A × B
15. Ra[fst(x);fst(y)]
16. Rb[snd(x);snd(y)]
17. Ra[fst(y);fst(x)]
18. Rb[snd(y);snd(x)]
19. (fst(x)) = (fst(y)) ∈ A
20. (snd(x)) = (snd(y)) ∈ B
⊢ x = y ∈ (A × B)
BY
{ (DVar `x' THEN DVar `y' THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  Ra  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  Rb  :  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
5.  Refl(A;a,a'.Ra[a;a'])
6.  Trans(A;a,a'.Ra[a;a'])
7.  AntiSym(A;a,a'.Ra[a;a'])
8.  Refl(B;b,b'.Rb[b;b'])
9.  Trans(B;b,b'.Rb[b;b'])
10.  AntiSym(B;b,b'.Rb[b;b'])
11.  Refl(A  \mtimes{}  B;x,y.Ra[fst(x);fst(y)]  \mwedge{}  ((\mneg{}((fst(x))  =  (fst(y))))  \mvee{}  Rb[snd(x);snd(y)]))
12.  Trans(A  \mtimes{}  B;x,y.Ra[fst(x);fst(y)]  \mwedge{}  ((\mneg{}((fst(x))  =  (fst(y))))  \mvee{}  Rb[snd(x);snd(y)]))
13.  x  :  A  \mtimes{}  B
14.  y  :  A  \mtimes{}  B
15.  Ra[fst(x);fst(y)]
16.  Rb[snd(x);snd(y)]
17.  Ra[fst(y);fst(x)]
18.  Rb[snd(y);snd(x)]
19.  (fst(x))  =  (fst(y))
20.  (snd(x))  =  (snd(y))
\mvdash{}  x  =  y


By

---

Latex:
(DVar  `x'  THEN  DVar  `y'  THEN  All  Reduce  THEN  Auto)

---

Home Index