% Lemma F2

lemmaF2(S,K,I) ==  ((0=<K and 0=<I) => (free(lift(S,K),I) <=>
 (( free(S,p(I)) and K < I) or (free(S,I) and I < K) ))).

%top_predicates_precedence([lemmaF2]).