Step
*
2
2
1
of Lemma
fpf-rename-cap2
1. A : Type
2. C : Type
3. B : Type
4. eqa : EqDecider(A)
5. eqc : EqDecider(C)
6. eqc' : EqDecider(C)
7. r : A ─→ C
8. f : a:A fp-> B
9. a : A
10. z : B
11. Inj(A;C;r)
12. ↑r a ∈ dom(rename(r;f))
⊢ ↑a ∈ dom(f)
BY
{ (((InstLemma `fpf-rename-dom` [⌈A⌉; ⌈C⌉; ⌈λ2a.B⌉; ⌈eqa⌉; ⌈eqc⌉; ⌈r⌉; ⌈f⌉; ⌈r a⌉])⋅ THENA Auto)
THEN (D (-1))
THEN ThinTrivial
THEN (Thin (-2))
THEN ExRepD) }
1
1. A : Type
2. C : Type
3. B : Type
4. eqa : EqDecider(A)
5. eqc : EqDecider(C)
6. eqc' : EqDecider(C)
7. r : A ─→ C
8. f : a:A fp-> B
9. a : A
10. z : B
11. Inj(A;C;r)
12. ↑r a ∈ dom(rename(r;f))
13. a@0 : A
14. ↑a@0 ∈ dom(f)
15. (r a) = (r a@0) ∈ C
⊢ ↑a ∈ dom(f)
Latex:
1. A : Type
2. C : Type
3. B : Type
4. eqa : EqDecider(A)
5. eqc : EqDecider(C)
6. eqc' : EqDecider(C)
7. r : A {}\mrightarrow{} C
8. f : a:A fp-> B
9. a : A
10. z : B
11. Inj(A;C;r)
12. \muparrow{}r a \mmember{} dom(rename(r;f))
\mvdash{} \muparrow{}a \mmember{} dom(f)
By
(((InstLemma `fpf-rename-dom` [\mkleeneopen{}A\mkleeneclose{}; \mkleeneopen{}C\mkleeneclose{}; \mkleeneopen{}\mlambda{}\msubtwo{}a.B\mkleeneclose{}; \mkleeneopen{}eqa\mkleeneclose{}; \mkleeneopen{}eqc\mkleeneclose{}; \mkleeneopen{}r\mkleeneclose{}; \mkleeneopen{}f\mkleeneclose{}; \mkleeneopen{}r a\mkleeneclose{}])\mcdot{} THENA Auto)
THEN (D (-1))
THEN ThinTrivial
THEN (Thin (-2))
THEN ExRepD)
Home
Index