At Sat, 04 May 2013 09:34:01 +0100, Jon Fairbairn wrote: > α-equivalence on the Böhm trees — normal forms extended to > infinity. I suppose that counts as “some semantics” but its very > direct. Ah yes, that makes sense. Thanks! Francesco