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