proposition: Lemma recurse_unguard_pf A ts (u : @unguarded_form A ts) : guard_ax ts (recurse_unguard_tag (untag u)) id_omap_fun.
proof: Proof. by case: u. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)