---

Step * of Lemma fpf-rename-cap

∀[A,C,B:Type]. ∀[eqa:EqDecider(A)]. ∀[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-ap` THEN Auto))) }

1
.....wf..... 
1. A : Type
2. C : Type
3. B : Type
4. eqa : EqDecider(A)
5. eqc : EqDecider(C)
6. r : A ─→ C
7. f : a:A fp-> B
8. a : A
9. z : B
10. 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. r : A ─→ C
7. f : a:A fp-> B
8. a : A
9. z : B
10. Inj(A;C;r)
11. ↑r a ∈ dom(rename(r;f))
12. ¬↑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. r : A ─→ C
7. f : a:A fp-> B
8. a : A
9. z : B
10. Inj(A;C;r)
11. ¬↑r a ∈ dom(rename(r;f))
12. ↑a ∈ dom(f)
⊢ z = f(a) ∈ B

---

Latex:


\mforall{}[A,C,B:Type].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[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-ap`  THEN  Auto)))

---

Home Index