---

{ [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) supposing ((c = (r a)) and Inj(A;C;r)) }

{ Proof }

---

Definitions occuring in Statement :  fpf-rename: rename(r;f),  fpf-cap: f(x)?z,  fpf: a:A fp-> B[a],  inject: Inj(A;B;f),  uimplies: b supposing a,  uall: [x:A]. B[x],  apply: f a,  function: x:A  B[x],  universe: Type,  equal: s = t,  deq: EqDecider(T)
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  member: t  T,  prop: ,  so_lambda: x.t[x],  all: x:A. B[x],  implies: P  Q,  so_apply: x[s]
Lemmas :  fpf-cap_wf,  inject_wf,  fpf_wf,  deq_wf,  fpf-rename-cap2,  fpf-rename_wf

---

\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))


Date html generated: 2011_08_10-AM-08_04_48
Last ObjectModification: 2011_06_18-AM-08_22_48

Home Index