proposition: Lemma start_pf i ts (f : form (empx U) i ts) : @raxiom i ts (untag f) (isundef i ts) (equate f).
proof: Proof. by case: f=>f [<- S A] /(isundef_sound A) /negbTE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)