+l
@[a:'prop'][b:'prop']
-imp:=[x:a]b:'prop'
+%modification by Guidi to avoid prop inclusion
+%imp:=[x:a]b:'prop' %original line
+imp:='prim':'prop'
+%end of modification
[a1:a][i:imp(a,b)]
-mp:=<a1>i:b
+%modification by Guidi to avoid prop inclusion
+%mp:=<a1>i:b %original line
+mp:='prim':b
+b@[f:[x:a]b] % we define modus tollens
+mt:='prim':imp(a,b)
+%end of modification
a@refimp:=[x:a]x:imp(a,a)
b@[c:'prop'][i:imp(a,b)][j:imp(b,c)]
trimp:=[x:a]<<x>i>j:imp(a,c)
a@not:=imp(con):'prop'
wel:=not(not(a)):'prop'
[a1:a]
-weli:=[x:not(a)]<a1>x:wel(a)
+weli:=[x:not(a)]<a1>x:wel(a) %original line
a@[w:wel(a)]
et:='prim':a
a@[c1:con]
thorec2:=oreci(c,b,thor2(orece1(c,a,o)),thec2(orece2(c,a,o))):orec(c,b)
-iff
@[sigma:'type'][p:[x:sigma]'prop']
-%suggestion by van Daalen to remove the first eta-reduction
+%modification by Guidi to remove prop inclusion
%all:=p:'prop' %original line
-all:=[x:sigma]<x>p:'prop'
-%end of suggestion
+%all:=[x:sigma]<x>p:'prop' %suggestion by van Daalen to remove eta-reduction
+all:='prim':'prop'
+%end of modification
[a1:all(sigma,p)][s:sigma]
-alle:=<s>a1:<s>p
+%modification by Guidi to remove prop inclusion
+%alle:=<s>a1:<s>p %original line
+alle:='prim':<s>p
+p@[f:[s:sigma]<s>p] % we define modus tollens
+alli:='prim':all(sigma,p)
+%end of modification
+all
p@[s:sigma][n:not(<s>p)]
th1:=[x:all(sigma,p)]<<s>x>n:not(all(sigma,p))
-all
p@non:=[x:sigma]not(<x>p):[x:sigma]'prop'
+%modification by Guidi to remove prop inclusion
+p@lppc0:='prim':'prop'
+%end of modification
some:=not(non(p)):'prop'
[s:sigma][sp:<s>p]
somei:=th1".all"(non(p),s,weli(<s>p,sp)):some(sigma,p)