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