{ norm-base-deriv() 
id-fun(BaseDef) }
{ Proof }
Definitions occuring in Statement :
norm-base-deriv: norm-base-deriv(),
base-deriv: BaseDef,
member: t T,
id-fun: id-fun(T)
Definitions :
id-fun: id-fun(T),
eclass: EClass(A[eo; e]),
equal: s = t,
member: t T,
function: x:A 
B[x],
all: 
x:A. B[x],
subtype_rel: A 
r B,
isect: 
x:A. B[x],
fpf: a:A fp-> B[a],
universe: Type,
limited-type: LimitedType,
bool: 
,
product: x:A 
B[x],
lambda: 
x.A[x],
strong-subtype: strong-subtype(A;B),
list: type List,
name: Name,
set: {x:A| B[x]} ,
exists: 
x:A. B[x],
intensional-universe: IType,
subtype: S T,
implies: P 
Q,
es-E-interface: E(X),
pair: <a, b>,
l_member: (x l),
norm-pair: norm-pair(Na;Nb),
apply: f a,
so_apply: x[s],
value-type: value-type(T),
Id: Id,
atom: Atom$n,
int: 
,
atom: Atom,
rec: rec(x.A[x]),
quotient: x,y:A//B[x; y],
tunion: 
x:A.B[x],
b-union: A B,
union: left + right,
tag-by: zT,
or: P 
Q,
rev_implies: P 
Q,
and: P 
Q,
iff: P Q,
ldag: LabeledDAG(T),
labeled-graph: LabeledGraph(T),
record: record(x.T[x]),
isect2: T1 T2,
nat: 
,
limited-type-level: limited-type-level{i:l}(n;T),
record+: record+,
fset: FSet{T},
top: Top,
true: True,
fpf-cap: f(x)?z,
assert: 
b,
guard: {T},
so_lambda: 
x.t[x],
not: 
A,
le: A 
B,
sq_type: SQType(T),
false: False,
prop: 
,
sq-id-fun: sq-id-fun(T),
norm-list: norm-list(N),
nil: [],
norm-base-deriv: norm-base-deriv(),
base-deriv: BaseDef,
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
MaAuto: Error :MaAuto,
Complete: Error :Complete,
Try: Error :Try,
D: Error :D,
CollapseTHENA: Error :CollapseTHENA,
tactic: Error :tactic,
Unfold: Error :Unfold
Lemmas :
name_wf,
norm-pair_wf,
norm-list_wf,
subtype_base_sq,
list-value-type,
product-value-type,
limited-type-level_wf,
nat_wf,
intensional-universe_wf,
value-type_wf,
atom2-value-type,
Id_wf,
member_wf,
bool_wf,
limited-type_wf,
id-fun_wf,
subtype_rel_wf
norm-base-deriv() \mmember{} id-fun(BaseDef)
Date html generated:
2011_08_17-PM-04_21_52
Last ObjectModification:
2011_06_18-AM-11_33_50
Home
Index