{ NameDeq 
EqDecider(Name) }
{ Proof }
Definitions occuring in Statement :
name-deq: NameDeq,
name: Name,
member: t T,
deq: EqDecider(T)
Definitions :
equal: s = t,
member: t T,
atom-deq: AtomDeq,
atom: Atom,
function: x:A 
B[x],
all: 
x:A. B[x],
list-deq: list-deq(eq),
name-deq: NameDeq,
name: Name,
Unfold: Error :Unfold,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic
Lemmas :
list-deq_wf,
atom-deq_wf
NameDeq \mmember{} EqDecider(Name)
Date html generated:
2010_08_26-PM-11_29_54
Last ObjectModification:
2010_02_15-PM-11_11_20
Home
Index