---

Step * 2 1 1 1 of Lemma set-elim


1. A : Type
2. B : A ⟶ Type
3. a : A
4. a2 : B[a]
5. (λp.(fst(p))) <a, a2> ∈ A
⊢ a2 ∈ B[fst(<a, a2>)]
BY
{ (RW (AddrC [1;2] (ComputeToC [])) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  a  :  A
4.  a2  :  B[a]
5.  (\mlambda{}p.(fst(p)))  <a,  a2>  \mmember{}  A
\mvdash{}  a2  \mmember{}  B[fst(<a,  a2>)]


By

---

Latex:
(RW  (AddrC  [1;2]  (ComputeToC  []))  0  THEN  Auto)

---

Home Index