---

{ [A,C:Type]. [B:A  Type]. [D:C  Type]. [rinv:C  (A?)]. [r:A  C].
  [f:c:C fp-> D[c]].
    (fpf-inv-rename(r;rinv;f)  a:A fp-> B[a]) supposing 
       ((a:A. (D[r a] = B[a])) and 
       inv-rel(A;C;r;rinv)) }

{ Proof }

---

Definitions occuring in Statement :  fpf-inv-rename: fpf-inv-rename(r;rinv;f),  fpf: a:A fp-> B[a],  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  all: x:A. B[x],  unit: Unit,  member: t  T,  apply: f a,  function: x:A  B[x],  union: left + right,  universe: Type,  equal: s = t,  inv-rel: inv-rel(A;B;f;finv)
Definitions :  uall: [x:A]. B[x],  fpf: a:A fp-> B[a],  so_apply: x[s],  uimplies: b supposing a,  all: x:A. B[x],  member: t  T,  fpf-inv-rename: fpf-inv-rename(r;rinv;f),  pi1: fst(t),  pi2: snd(t),  prop: ,  so_lambda: x.t[x],  assert: b,  btrue: tt,  ifthenelse: if b then t else f fi ,  true: True,  compose: f o g,  implies: P  Q,  isl: isl(x),  outl: outl(x),  bfalse: ff,  sq_type: SQType(T),  guard: {T},  exists: x:A. B[x],  and: P  Q,  cand: A c B,  iff: P  Q,  inv-rel: inv-rel(A;B;f;finv),  false: False
Lemmas :  l_member_wf,  inv-rel_wf,  fpf_wf,  unit_wf,  mapfilter_wf,  isl_wf,  outl_wf,  subtype_base_sq,  bool_wf,  bool_subtype_base,  assert_wf,  assert_elim,  member_map_filter,  true_wf,  false_wf

---

\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[D:C  {}\mrightarrow{}  Type].  \mforall{}[rinv:C  {}\mrightarrow{}  (A?)].  \mforall{}[r:A  {}\mrightarrow{}  C].  \mforall{}[f:c:C  fp->  D[c]].
    (fpf-inv-rename(r;rinv;f)  \mmember{}  a:A  fp->  B[a])  supposing 
          ((\mforall{}a:A.  (D[r  a]  =  B[a]))  and 
          inv-rel(A;C;r;rinv))


Date html generated: 2011_08_10-AM-08_04_54
Last ObjectModification: 2011_06_18-AM-08_22_51

Home Index