---

Step * of Lemma equipollent-singleton-domain

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

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

---

Latex:

---

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


By

---

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

---

Home Index