---

Step * of Lemma equipollent-identity

∀[A,B:Type].  (B ~ Unit ⇒ B × A ~ A)
BY
{ ((Auto THEN With ⌜λx.(snd(x))⌝ (D 0)⋅) THEN Auto THEN RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto))) }

1
1. A : Type
2. B : Type
3. B ~ Unit@i
4. a1 : B × A@i
5. a2 : B × A@i
6. (snd(a1)) = (snd(a2)) ∈ A@i
⊢ a1 = a2 ∈ (B × A)

2
1. [A] : Type
2. [B] : Type
3. B ~ Unit@i
4. b : A@i
⊢ ∃a:B × A. ((snd(a)) = b ∈ A)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    (B  \msim{}  Unit  {}\mRightarrow{}  B  \mtimes{}  A  \msim{}  A)


By

---

Latex:
((Auto  THEN  With  \mkleeneopen{}\mlambda{}x.(snd(x))\mkleeneclose{}  (D  0)\mcdot{})  THEN  Auto  THEN  RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto)))

---

Home Index