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