---

Step * of Lemma equipollent-singleton-domain2

No Annotations
∀[S:Type]. (singleton-type(S) ⇒ (∀[A:Type]. S ⟶ A ~ A))
BY
{ ((Auto THEN D 2) THEN RenameVar `u' 2 THEN (BLemma `equipollent_inversion` THENA Auto)) }

1
1. [S] : Type
2. u : S
3. ∀a':S. (a' = u ∈ S)
4. [A] : Type
⊢ A ~ S ⟶ A

---

Latex:

---

Latex:
No  Annotations
\mforall{}[S:Type].  (singleton-type(S)  {}\mRightarrow{}  (\mforall{}[A:Type].  S  {}\mrightarrow{}  A  \msim{}  A))


By

---

Latex:
((Auto  THEN  D  2)  THEN  RenameVar  `u'  2  THEN  (BLemma  `equipollent\_inversion`  THENA  Auto))

---

Home Index