1te1(\(A,@(*(A),^(j))),sub,m,[],[],2,3) 2te1(\(A,@(*(A),^(j))),sub,m,[sub(\(B,@(*(B),^(m))),C,f)],[],2,3) 3te1(\(A,@(*(A),^(m))),sub,f,[],[],0,1) 4te1(\(A,exists(B,/\(@(unicorn,B),@(*(A),B)))),obj,n,[],[],4,6) 5te1(\(A,exists(B,/\(@(unicorn,B),@(*(A),B)))),obj,n,[sub(\(C,@(*(C),^(j))),D,m)],[],4,6) 6te1(\(A,exists(B,/\(@(unicorn,B),@(*(A),B)))),obj,n,[sub(\(C,@(*(C),^(m))),D,f),sub(\(E,@(*(E),^(j))),F,m)],[],4,6) 7te1(\(A,exists(B,/\(@(unicorn,B),@(*(A),B)))),obj,n,[sub(\(C,@(*(C),^(m))),D,f)],[],4,6) 8