---

Step * of Lemma fpf-rename-cap2

∀[A,C,B:Type]. ∀[eqa:EqDecider(A)]. ∀[eqc,eqc':EqDecider(C)]. ∀[r:A ─→ C]. ∀[f:a:A fp-> B]. ∀[a:A]. ∀[z:B].
  rename(r;f)(r a)?z = f(a)?z ∈ B supposing Inj(A;C;r)
BY
{ (((Auto THEN Unfold `fpf-cap` 0 THEN SplitOnConclITE) THENA Try (Complete (Auto)))
   THEN Try ((SplitOnConclITE THEN Auto))
   THEN Try ((BLemma `fpf-rename-ap2` THEN Auto))) }

1
.....wf..... 
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)
⊢ r a ∈ dom(rename(r;f)) ∈ 𝔹

2
.....falsecase..... 
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 ∈ dom(f)
⊢ rename(r;f)(r a) = z ∈ B

3
.....truecase..... 
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 ∈ dom(f)
⊢ z = f(a) ∈ B

---

Latex:


\mforall{}[A,C,B:Type].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[eqc,eqc':EqDecider(C)].  \mforall{}[r:A  {}\mrightarrow{}  C].  \mforall{}[f:a:A  fp->  B].  \mforall{}[a:A].
\mforall{}[z:B].
    rename(r;f)(r  a)?z  =  f(a)?z  supposing  Inj(A;C;r)


By

(((Auto  THEN  Unfold  `fpf-cap`  0  THEN  SplitOnConclITE)  THENA  Try  (Complete  (Auto)))
  THEN  Try  ((SplitOnConclITE  THEN  Auto))
  THEN  Try  ((BLemma  `fpf-rename-ap2`  THEN  Auto)))

---

Home Index