---

Step * 1 of Lemma pair_eta_rw


1. A : Type
2. B : A ⟶ Type
3. p : a:A × B[a]
⊢ <fst(p), snd(p)> = p ∈ (a:A × B[a])
BY
{ (D 3 THEN AbReduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  p  :  a:A  \mtimes{}  B[a]
\mvdash{}  <fst(p),  snd(p)>  =  p


By

---

Latex:
(D  3  THEN  AbReduce  0  THEN  Auto)

---

Home Index