Step
*
2
1
of Lemma
mono-list
.....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))
BY
{ ((D 0 THENA Auto) THEN D -1 THEN D -2) }
1
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. [] = [u / v] ∈ (A List)
⊢ [] ∈ 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. u1 : A
9. v1 : A List
10. [u1 / v1] = [u / v] ∈ (A List)
⊢ [u1 / v1] ∈ A × (A List)
Latex:
Latex:
.....antecedent.....
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{} \{x:A List| x = [u / v]\} \msubseteq{}r (A \mtimes{} (A List))
By
Latex:
((D 0 THENA Auto) THEN D -1 THEN D -2)
Home
Index