proposition: Lemma recurse_guard_pf A B C ts (f : omap_fun (nat_mapUMC B) (nat_mapUMC C)) (g : @guarded_form A B ts) : guard_ax ts (recurse_guard_tag (f (untag g))) (comp_omap_fun (guard_of g) f).
proof: Proof. by case: g=>e g pf /=; rewrite pf. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)