---

Step * 2 1 2 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
6. ((λp.Ax) a2) = ((λp.Ax) a2) ∈ Image(B[fst(<a, a2>)],(λp.Ax))
⊢ Ax ∈ ↓B[fst(<a, a2>)]
BY
{ (Reduce (-1) 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
6.  ((\mlambda{}p.Ax)  a2)  =  ((\mlambda{}p.Ax)  a2)
\mvdash{}  Ax  \mmember{}  \mdownarrow{}B[fst(<a,  a2>)]


By

---

Latex:
(Reduce  (-1)  THEN  Auto)\mcdot{}

---

Home Index