te1(\(A,@(*(A),^(j))),sub,m,[],[],0,1)
te1(\(A,exists(B,/\(@(unicorn,B),@(*(A),B)))),obj,n,[],[],2,4)
te1(\(A,exists(B,/\(@(unicorn,B),@(*(A),B)))),obj,n,[sub(\(C,@(*(C),^(j))),D,m)],[],2,4)