1 # The lambda-term \omega
2 # This book is not accepted in AUT-QE because [y:'type'] is not allowed
3 # This book is accepted in lambda-delta with sort inclusion but omega is not
4 # valid if sort inclusion is allowed on the term backbone only
5 # This book is valid in lambda-delta with sort inclusion allowed everywhere
8 @ delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
9 omega := <delta>delta : 'type'