proposition: Lemma omfX A B C ts (f : omap_fun (nat_mapUMC B) (nat_mapUMC C)) (g : @guarded_form A B ts) : valid (omf_interp id_omap_fun ts) -> f (untag g) = omf_interp (comp_omap_fun (guard_of g) f) ts.
proof: Proof. case: g=>eq g /=; elim: ts eq=>[|s a|ts1 IH1 ts2 IH2|t] /= eq pf V. - by rewrite pf !omf_unit. - rewrite validPt in V; rewrite pf omfPt // /obind /oapp /=. by case: (OmapFun.mfunc _ _)=>[x|] //; rewrite ?omfPt ?omf_unit. - rewrite pf /= !omfUn //; last by rewrite -omfUn ?valid_omf. by rewrite IH1 ?(validL V) // IH2 ?(validR V). by rewrite pf. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)