---

Step * of Lemma fpf-rename-cap3

∀[A,C,B:Type]. ∀[eqa:EqDecider(A)]. ∀[eqc,eqc':EqDecider(C)]. ∀[r:A ⟶ C]. ∀[f:a:A fp-> B]. ∀[a:A]. ∀[z:B]. ∀[c:C].
  (rename(r;f)(c)?z = f(a)?z ∈ B) supposing ((c = (r a) ∈ C) and Inj(A;C;r))
BY
{ ((Auto THEN (HypSubst (-1) 0)) THENA Auto) }

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. c : C
12. Inj(A;C;r)
13. c = (r a) ∈ C
⊢ rename(r;f)(r a)?z = f(a)?z ∈ B

2
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. c : C
12. Inj(A;C;r)
13. c = (r a) ∈ C
14. z1 : C
⊢ rename(r;f)(z1)?z ∈ B

---

Latex:

---

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].  \mforall{}[c:C].
    (rename(r;f)(c)?z  =  f(a)?z)  supposing  ((c  =  (r  a))  and  Inj(A;C;r))


By

---

Latex:
((Auto  THEN  (HypSubst  (-1)  0))  THENA  Auto)

---

Home Index