% 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))).

% Lemma F1
lemmaF1(S,T,U,I) == ((~free(S,I) and 0=<I) => (subst(S,I,T) = subst(S,I,U))).

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