Step
*
2
of Lemma
mono-list
1. A : Type
2. mono(A)
3. u : A
4. v : A List
5. ∀b:Base. (is-above(A List;v;b)
⇒ (v = b ∈ (A List)))
6. b : Base
7. is-above(A List;[u / v];b)
⊢ [u / v] = b ∈ (A List)
BY
{ (InstLemma `is-above-singleton-subtype` [⌜A List⌝;⌜[u / v]⌝;⌜A × (A List)⌝;⌜b⌝]⋅ THENA Auto) }
1
.....antecedent.....
1. A : Type
2. mono(A)
3. u : A
4. v : A List
5. ∀b:Base. (is-above(A List;v;b)
⇒ (v = b ∈ (A List)))
6. b : Base
7. is-above(A List;[u / v];b)
⊢ {x:A List| x = [u / v] ∈ (A List)} ⊆r (A × (A List))
2
1. A : Type
2. mono(A)
3. u : A
4. v : A List
5. ∀b:Base. (is-above(A List;v;b)
⇒ (v = b ∈ (A List)))
6. b : Base
7. is-above(A List;[u / v];b)
8. is-above(A × (A List);[u / v];b)
⊢ [u / v] = b ∈ (A List)
Latex:
Latex:
1. A : Type
2. mono(A)
3. u : A
4. v : A List
5. \mforall{}b:Base. (is-above(A List;v;b) {}\mRightarrow{} (v = b))
6. b : Base
7. is-above(A List;[u / v];b)
\mvdash{} [u / v] = b
By
Latex:
(InstLemma `is-above-singleton-subtype` [\mkleeneopen{}A List\mkleeneclose{};\mkleeneopen{}[u / v]\mkleeneclose{};\mkleeneopen{}A \mtimes{} (A List)\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{} THENA Auto)
Home
Index