rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> 
ext atom by intro atom
.
H >> atom in 
by intro
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> atom ext "
" by intro "
"
.
H >> "
" in atom by intro
where `
' is any sequence of prl characters.
.
H >> atom_eq(a;b;t;
) in T by intro
*
>> a in atom
*
>> b in atom
*
a=b in atom >> t in T
*
(a=b in atom)->void >> 
in T
rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex
.
H >> atom_eq(a;a;t;
)=
in T by reduce 1
*
>> t=
in T
where a is a canonical token term.
.
H >> atom_eq(a;b;t;
)=
in T by reduce 1
*
>> 
=
in T
where a and b are different canonical token terms.