[ new ] Untyped equality test: lazy eta-expansion
[ fix ] Slightly smaller reification for variables