{ 
[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]) }
{ Proof }
Definitions occuring in Statement :
fpf-rename: rename(r;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],
member: t T,
apply: f a,
function: x:A B[x],
universe: Type,
equal: s = t,
deq: EqDecider(T)
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-rename: rename(r;f),
pi1: fst(t),
pi2: snd(t),
prop: 
,
so_lambda: 
x.t[x],
implies: P 
Q,
exists: 
x:A. B[x],
and: P 
Q,
cand: A c B,
iff: P 
Q,
rev_implies: P Q
Lemmas :
map_wf,
l_member_wf,
fpf_wf,
deq_wf,
hd-filter,
eqof_wf,
member_map,
assert_wf,
iff_weakening_uiff,
uiff_inversion,
deq_property
\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:
2011_08_10-AM-08_04_11
Last ObjectModification:
2011_06_18-AM-08_22_30
Home
Index