proposition: Lemma start_pf j k ts tg (fg : form j k tg) : @raxiom j k ts (untag fg) (obind (pprint k \o rev) (subtract tg ts [::])) (equate fg).
proof: Proof. case: fg=>fg [Eg S Ag]; case E: (subtract _ _ _)=>[rs|] //= Am _; split=>//. move/(subtract_sound Ag (sc_wf S Am)): E=>/=. by rewrite unitR joinC Eg pp_interp interp_rev. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)