use(reflecttrees).

goal
~ all(S,all(T,all(P,
     tree(S) and tree(T) and path(P) and subtree(S,P,T) =>
	exists(S1,exists(T1,exists(P1,
	 tree(S1) and tree(T1) and path(P1) 
	 and mirror(S,S1) and mirror(T,T1) and reflect(P,P1) and
	     subtree(S1,P1,T1))))))).