Step
*
of Lemma
atom2-value-type
value-type(Atom2)
BY
{ TACTIC:(ValueTypeAuto THEN Refine_callbyvalueAtom2 THEN Trivial) }
Latex:
Latex:
value-type(Atom2)
By
Latex:
TACTIC:(ValueTypeAuto  THEN  Refine\_callbyvalueAtom2  THEN  Trivial)
Home
Index