Step
*
of Lemma
base-equal-partial
∀[A:Type]
∀[a,b:Base].
a = b ∈ partial(A) supposing (((a)↓
⇐⇒ (b)↓) ∧ a = b ∈ A supposing (a)↓) ∧ (¬is-exception(a)) ∧ (¬is-exception(b))
supposing value-type(A)
BY
{ (RepeatFor 4 ((UD THENA Auto)) THEN (At ⌜Type⌝ (D 0)⋅ THENA (InstLemma `equal-wf-base` [⌜A⌝;⌜a⌝;⌜b⌝]⋅ THEN Auto))) }
1
1. A : Type
2. value-type(A)
3. a : Base
4. b : Base
5. (((a)↓
⇐⇒ (b)↓) ∧ a = b ∈ A supposing (a)↓) ∧ (¬is-exception(a)) ∧ (¬is-exception(b))
⊢ a = b ∈ partial(A)
Latex:
Latex:
\mforall{}[A:Type]
\mforall{}[a,b:Base].
a = b
supposing (((a)\mdownarrow{} \mLeftarrow{}{}\mRightarrow{} (b)\mdownarrow{}) \mwedge{} a = b supposing (a)\mdownarrow{}) \mwedge{} (\mneg{}is-exception(a)) \mwedge{} (\mneg{}is-exception(b))
supposing value-type(A)
By
Latex:
(RepeatFor 4 ((UD THENA Auto))
THEN (At \mkleeneopen{}Type\mkleeneclose{} (D 0)\mcdot{} THENA (InstLemma `equal-wf-base` [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{} THEN Auto))
)
Home
Index