% Lemma 1
lemma1(T,I,K) == (I<s(K) => lift(lift(T,I),s(K))=lift(lift(T,K),I)).


% Lemma 2
lemma2(T,S,J,I) == 
       (J<s(I) and 0=<J  => lift(subst(T,J,S),I) = subst(lift(T,s(I)),J,lift(S,I))).



% Lemma 3
lemma3(T,S,I,J) ==
       (I<s(J) and 0=<I => 
		lift(subst(T,J,S),I) = subst(lift(T,I),s(J),lift(S,I))).


% Lemma 4
lemma4(T,S,K) == (subst(lift(T,K),K,S) = T).


% Lemma 5
lemma5(T,U,V,I,J) ==
   	(I<s(J) and 0=<I =>
	  	subst(subst(T,s(J),lift(V,I)),I,subst(U,J,V)) = 
		subst(subst(T,I,U),J,V)).




% Lemma 6
lemma6(T,I)== (0=<I => subst(T,I,var(I))=subst(T,s(I),var(I))).



/*
% flat variants
lemma1f(T,I,K) == 
	all(LTI,all(LKT,
		(I<s(K) 
		and lift(T,I)=LTI
		and lift(T,K)=LTK =>
			lift(LTI,s(K))=lift(LTK,I)))).

lemma2f(T,S,J,I) == 
       all(TJS,all(LTsI,all(LSI,
	(J<s(I) and 0=<J
	       and subst(T,J,S)=TJS 
	       and lift(T,s(I))=LTsI 
	       and lift(S,I)=LSI => 
		lift(TJS,I) = subst(LTsI,J,LSI))))).

lemma3f(T,S,I,J) ==
       all(TJS,all(LTI,all(LSI,
	(I<s(J) and 0=<I 
	       and subst(T,J,S)=TJS 
	       and lift(T,I)=LTI 
	       and lift(S,I)=LSI => 
		lift(TJS,I) = subst(LTI,s(J),LSI))))).

lemma3f1(T,S,I,J) ==
       all(TJS,all(LTI,
	(I<s(J) and 0=<I 
		and subst(T,J,S)=TJS 
		and lift(T,I)=LTI 
	        => 
		lift(TJS,I) = subst(LTI,s(J),lift(S,I))))).


lemma4f(T,S,K) == all(K1,(K=K1 => subst(lift(T,K),K1,S) = T)).



top_predicates_precedence([lemma6,lemma4,lemma3,lemma2,lemma1,lemma4f,lemma3f,lemma3f1,lemma2f,lemma1f]).
*/


top_predicates_precedence([lemma6,lemma4,lemma3,lemma2,lemma1]).