---

Step * 1 of Lemma e-isect_wf


1. A : Base
2. A1 : Base
3. A = A1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
4. A ∈ Type
5. A1 ∈ Type
6. A ≡ A1
7. B : Base
8. B1 : Base
9. B = B1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
10. B ∈ Type
11. B1 ∈ Type
12. B ≡ B1
⊢ A ⋂ B ≡ A1 ⋂ B1
BY
{ (D 0 THEN (D 0 THENA Auto) THEN D -1 THEN (Isect2CD THENL [DoSubsume; (Thin (-1) THEN DoSubsume)]) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Base
2.  A1  :  Base
3.  A  =  A1
4.  A  \mmember{}  Type
5.  A1  \mmember{}  Type
6.  A  \mequiv{}  A1
7.  B  :  Base
8.  B1  :  Base
9.  B  =  B1
10.  B  \mmember{}  Type
11.  B1  \mmember{}  Type
12.  B  \mequiv{}  B1
\mvdash{}  A  \mcap{}  B  \mequiv{}  A1  \mcap{}  B1


By

---

Latex:
(D  0
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (Isect2CD  THENL  [DoSubsume;  (Thin  (-1)  THEN  DoSubsume)])
  THEN  Auto)

---

Home Index