# Copyright (C) 1977, L.S. van Benthem Jutting
# 1992, revised by F. Wiedijk (http://www.cs.ru.nl/~freek/aut/)
# 2008, revised by F. Guidi to remove the eta-reductions
+# 2014, revised by F. Guidi to suggest @-typing removal
+l
@[a:'prop'][b:'prop']
b@ec:=[x:a]not(<x>b):'prop'
[n:not(a)]
eci1:=[x:a]cone(not(<x>b),mp"l"(a,con,x,n)):ec(a,b)
-b@[a1:and(a,b)]
-ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b
+%suggestion by Guidi to remove @-typing
+b@[a1:and(a,b)] %original line
+ande2:=<ande1(a,b,a1)>ande2"l"(a,b,a1):<ande1(a,b,a1)>b %original line
+%b@[a1:and(a,[x:a]<x>b)]
+%ande2:=<ande1(a,[x:a]<x>b,a1)>ande2"l"(a,[x:a]<x>b,a1):<ande1(a,[x:a]<x>b,a1)>[x:a]<x>b
+%end of suggestion
a@[ksi:'type']
+ite
[x1:ksi][y1:ksi]