is mentioned by

Thm* r:rel(), I:Fmla, A:ioa{i:l}(), a:Label. covers_pred(A;I) r I (r':rel(). r' col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r))	[covers_pred_lemma2]
Thm* Q:Fmla, A:ioa{i:l}(). covers_pred(A;(Q)') covers_pred(A;Q)	[covers_pred_addprime]
Thm* A:ioa{i:l}(), I:Fmla, r:rel(). r I covers_pred(A;I) covers_rel(A;r)	[covers_pred_rel_member]

Try larger context: GenAutomata