Step * 2 of Lemma decidable__equal_union


1. [A] Type
2. [B] Type
3. ∀x,y:A.  Dec(x y ∈ A)
4. ∀u,v:B.  Dec(u v ∈ B)
5. x1 A
6. y1 B
⊢ Dec((inl x1) (inr y1 ) ∈ (A B))
BY
(Unfold `decidable` THEN OrRight THEN Auto THEN Obvious) }


Latex:


Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  \mforall{}x,y:A.    Dec(x  =  y)
4.  \mforall{}u,v:B.    Dec(u  =  v)
5.  x1  :  A
6.  y1  :  B
\mvdash{}  Dec((inl  x1)  =  (inr  y1  ))


By


Latex:
(Unfold  `decidable`  0  THEN  OrRight  THEN  Auto  THEN  Obvious)




Home Index