is mentioned by

Thm* A:ioa{i:l}(), rho:Decl, de:sig(), act:([[A.da]] rho), r,r0:rel(). tc_ioa(A;de) r smts_eff_rel(action_effect(kind(act);A.eff;A.frame);r0) rel_eq(rel_unprime(r);rel_unprime(r0)) (t:dec(). t A.da & t.lbl = kind(act))	[rel_effect_lemma]
Def wp_rel(A;a;r) == smts_eff_rel(action_effect(a;A.eff;A.frame);r)	[wp_rel]
Def smts_eff_pred(ss;p) == (rp.smts_eff_rel(ss;r))	[smts_eff_pred]

Try larger context: GenAutomata