pathologic @-typing removed by adding imp-introduction

diff --git a/helm/software/helena/examples/grundlagen/grundlagen.aut b/helm/software/helena/examples/grundlagen/grundlagen.aut
index d38532d369ee0903476d1406f88bd83b3af51f1b..d4d9528e8bf876a9478664df076f59bfd50b4dfc 100644 (file)
--- a/helm/software/helena/examples/grundlagen/grundlagen.aut
+++ b/helm/software/helena/examples/grundlagen/grundlagen.aut
@@ -682,11 +682,11 @@ th2:=[x:a]cone(<x>b,mp"l"(a,con,x,n)):imp(a,b)
 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)
-%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
+%suggestion by Guidi to remove @-typing by adding imp-introduction
+%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,imp(a,b))]
+ande2:=<ande1(a,imp(a,b),a1)>ande2"l"(a,imp(a,b),a1):<ande1(a,imp(a,b),a1)>b
 %end of suggestion
 a@[ksi:'type']
 +ite