helm/software/lambda-delta/automath/Omega.aut

   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 unrestricted sort inclusion
   6
   7 +l
   8 @ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
   9   Omega := <Delta>Delta             : 'type'
  10 -l