### Nuprl Lemma : fpf-rename_wf

`∀[A,C:Type]. ∀[B:A ─→ Type]. ∀[D:C ─→ Type]. ∀[eq:EqDecider(C)]. ∀[r:A ─→ C]. ∀[f:a:A fp-> B[a]].`
`  rename(r;f) ∈ c:C fp-> D[c] supposing ∀a:A. (D[r a] = B[a] ∈ Type)`

Proof

Definitions occuring in Statement :  fpf-rename: `rename(r;f)` fpf: `a:A fp-> B[a]` deq: `EqDecider(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` member: `t ∈ T` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T`
Lemmas :  l_member_wf subtype_rel-equal iff_weakening_equal equal_wf hd-filter member_map safe-assert-deq assert_wf
\mforall{}[A,C:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[D:C  {}\mrightarrow{}  Type].  \mforall{}[eq:EqDecider(C)].  \mforall{}[r:A  {}\mrightarrow{}  C].  \mforall{}[f:a:A  fp->  B[a]].
rename(r;f)  \mmember{}  c:C  fp->  D[c]  supposing  \mforall{}a:A.  (D[r  a]  =  B[a])

Date html generated: 2015_07_17-AM-11_10_38
Last ObjectModification: 2015_02_04-PM-05_15_05

Home Index