---

Step * 1 of Lemma isect_prod_lemma

.....subterm..... T:t
1:n
1. A : Type
2. B : Type
3. C : Type
4. x : A × B ⋂ A × C
⊢ x ∈ A × B ⋂ C
BY
{ Isect2HD 4 }

1
1. A : Type
2. B : Type
3. C : Type
4. x : A × B ⋂ A × C
5. x ∈ A × C
6. x ∈ A × B
⊢ x ∈ A × B ⋂ C

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  x  :  A  \mtimes{}  B  \mcap{}  A  \mtimes{}  C
\mvdash{}  x  \mmember{}  A  \mtimes{}  B  \mcap{}  C


By

---

Latex:
Isect2HD  4

---

Home Index