Step * 1 of Lemma assert-product-deq


1. Type
2. Type
3. EqDecider(A)
4. EqDecider(B)
5. x1 A
6. x2 B
7. y1 A
8. y2 B
9. <x1, x2> = <y1, y2> ∈ (A × B)
⊢ x1 y1 ∈ A
BY
((EqHD (-1) THENA Auto) THEN All Reduce THEN Auto) }


Latex:


Latex:

1.  A  :  Type
2.  B  :  Type
3.  a  :  EqDecider(A)
4.  b  :  EqDecider(B)
5.  x1  :  A
6.  x2  :  B
7.  y1  :  A
8.  y2  :  B
9.  <x1,  x2>  =  <y1,  y2>
\mvdash{}  x1  =  y1


By


Latex:
((EqHD  (-1)  THENA  Auto)  THEN  All  Reduce  THEN  Auto)




Home Index