---

Step * 2 of Lemma set-elim


1. A : Type
2. B : A ⟶ Type
3. [%] : a:A × B[a]
4. (λp.(fst(p))) % ∈ A
⊢ ↓B[(λp.(fst(p))) %]
BY
{ (UseWitness ⌜Ax⌝⋅ THEN D 3 THEN Reduce 0) }

1
1. A : Type
2. B : A ⟶ Type
3. a : A
4. B[a]
5. (λp.(fst(p))) <a, %2> ∈ A
⊢ Ax ∈ ↓B[fst(<a, %2>)]

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  [\%]  :  a:A  \mtimes{}  B[a]
4.  (\mlambda{}p.(fst(p)))  \%  \mmember{}  A
\mvdash{}  \mdownarrow{}B[(\mlambda{}p.(fst(p)))  \%]


By

---

Latex:
(UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  D  3  THEN  Reduce  0)

---

Home Index