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* c:(LabelCollection(Term)), r,r':rel(). r' col_subst2(c;r) (as:(LabelTerm) List. 1of(unzip(as)) = rel_primed_vars(r) & (i:. i < ||as|| 2of(as[i]) c(1of(as[i]))) & r' = rel_subst2(as;r))	[member_col_subst2]
Def wp2_rel(A;a;r) == col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r)	[wp2_rel]
Def wp2(A;a;Q) == (rQ.col_subst2(x.smts_eff(action_effect(a;A.eff;A.frame);x);r))	[wp2]

Try larger context: GenAutomata