reduction: simple implementation of whd1
reduction: simple implementation of whd1

This is useful to structure code as follows:
  foo (lam ...) :- ..
  foo T :- whd1 T T1, !, foo T1.
  foo _ :- error "not a lam".

LPCIC/coq-elpi