---

Step * 2 1 of Lemma isect2_decomp


1. t1 : Type
2. t2 : Type
3. x : ⋂b:𝔹. if b then t1 else t2 fi 
⊢ x ∈ t2
BY
{ (Refine_isectElimination 3 ff `x1' `x2' THEN Auto) }

---

Latex:

---

Latex:

1.  t1  :  Type
2.  t2  :  Type
3.  x  :  \mcap{}b:\mBbbB{}.  if  b  then  t1  else  t2  fi 
\mvdash{}  x  \mmember{}  t2


By

---

Latex:
(Refine\_isectElimination  3  ff  `x1'  `x2'  THEN  Auto)

---

Home Index