---

Step * of Lemma dep-isect-assoc

∀A:Type. ∀B:A ⟶ Type. ∀C:a:A ⟶ B[a] ⟶ Type.  a:A ⋂ b:B[a] ⋂ C[a;b] ≡ z:a:A ⋂ B[a] ⋂ C[z;z]
BY
{ (Auto THEN D 0 THEN At ⌜𝕌'⌝ (D 0)⋅) }

1
.....subterm..... T:t
1:n
1. A : Type
2. B : A ⟶ Type
3. C : a:A ⟶ B[a] ⟶ Type
4. x : a:A ⋂ b:B[a] ⋂ C[a;b]
⊢ x ∈ z:a:A ⋂ B[a] ⋂ C[z;z]

2
.....eq aux..... 
1. A : Type
2. B : A ⟶ Type
3. C : a:A ⟶ B[a] ⟶ Type
⊢ istype(a:A ⋂ b:B[a] ⋂ C[a;b])

3
.....subterm..... T:t
1:n
1. A : Type
2. B : A ⟶ Type
3. C : a:A ⟶ B[a] ⟶ Type
4. x : z:a:A ⋂ B[a] ⋂ C[z;z]
⊢ x ∈ a:A ⋂ b:B[a] ⋂ C[a;b]

4
.....eq aux..... 
1. A : Type
2. B : A ⟶ Type
3. C : a:A ⟶ B[a] ⟶ Type
⊢ istype(z:a:A ⋂ B[a] ⋂ C[z;z])

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}B:A  {}\mrightarrow{}  Type.  \mforall{}C:a:A  {}\mrightarrow{}  B[a]  {}\mrightarrow{}  Type.    a:A  \mcap{}  b:B[a]  \mcap{}  C[a;b]  \mequiv{}  z:a:A  \mcap{}  B[a]  \mcap{}  C[z;z]


By

---

Latex:
(Auto  THEN  D  0  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (D  0)\mcdot{})

---

Home Index