Step
*
1
2
1
1
1
1
of Lemma
simple-loc-comb2-classrel
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ C
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
11. v ∈ λl,w. lifting2-loc(f;l;w 0;w 1)|Loc; λz.[X; Y][z]|(e)
12. vs : k:ℕ2 ─→ [A; B][k]
13. ∀k:ℕ2. vs[k] ∈ [X; Y][k](e)
14. v = (f loc(e) (vs 0) (vs 1)) ∈ C
15. v ∈ λl,w. lifting2-loc(f;l;w 0;w 1)|Loc; λ2k.[X; Y][k]|(e)
⊢ ∃a:A. ∃b:B. (a ∈ X(e) ∧ b ∈ Y(e) ∧ (v = (f loc(e) a b) ∈ C))
BY
{ (InstConcl [⌈vs 0⌉;⌈vs 1⌉]⋅ THEN Auto THEN Auto') }
1
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ C
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
11. v ∈ λl,w. lifting2-loc(f;l;w 0;w 1)|Loc; λz.[X; Y][z]|(e)
12. vs : k:ℕ2 ─→ [A; B][k]
13. ∀k:ℕ2. vs[k] ∈ [X; Y][k](e)
14. v = (f loc(e) (vs 0) (vs 1)) ∈ C
15. v ∈ λl,w. lifting2-loc(f;l;w 0;w 1)|Loc; λ2k.[X; Y][k]|(e)
⊢ vs 0 ∈ X(e)
2
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id ─→ A ─→ B ─→ C
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
11. v ∈ λl,w. lifting2-loc(f;l;w 0;w 1)|Loc; λz.[X; Y][z]|(e)
12. vs : k:ℕ2 ─→ [A; B][k]
13. ∀k:ℕ2. vs[k] ∈ [X; Y][k](e)
14. v = (f loc(e) (vs 0) (vs 1)) ∈ C
15. v ∈ λl,w. lifting2-loc(f;l;w 0;w 1)|Loc; λ2k.[X; Y][k]|(e)
16. vs 0 ∈ X(e)
⊢ vs 1 ∈ Y(e)
Latex:
Latex:
1. Info : Type
2. A : Type
3. B : Type
4. C : Type
5. f : Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} C
6. X : EClass(A)
7. Y : EClass(B)
8. es : EO+(Info)
9. e : E
10. v : C
11. v \mmember{} \mlambda{}l,w. lifting2-loc(f;l;w 0;w 1)|Loc; \mlambda{}z.[X; Y][z]|(e)
12. vs : k:\mBbbN{}2 {}\mrightarrow{} [A; B][k]
13. \mforall{}k:\mBbbN{}2. vs[k] \mmember{} [X; Y][k](e)
14. v = (f loc(e) (vs 0) (vs 1))
15. v \mmember{} \mlambda{}l,w. lifting2-loc(f;l;w 0;w 1)|Loc; \mlambda{}\msubtwo{}k.[X; Y][k]|(e)
\mvdash{} \mexists{}a:A. \mexists{}b:B. (a \mmember{} X(e) \mwedge{} b \mmember{} Y(e) \mwedge{} (v = (f loc(e) a b)))
By
Latex:
(InstConcl [\mkleeneopen{}vs 0\mkleeneclose{};\mkleeneopen{}vs 1\mkleeneclose{}]\mcdot{} THEN Auto THEN Auto')
Home
Index