helm/software/helena/examples/automath/Omega.aut

   1 # The term \Omega
   2 # This book is not valid in AUT-QE because [y:'type'] is not allowed
   3 # This book is not valid in \lambda\delta < 3 because sort inclusion is not allowed
   4 # This book is not valid in \lambda\delta 3 because of two \upsilon-reductions on layer 1
   5
   6 +l
   7 @ Delta := [x:[y:'type']'type']<x>x : [x:[y:'type']'type']'type'
   8   Omega := <Delta>Delta             : 'type'
   9 -l