proposition: Lemma start_pf j k ts1 ts2 (f2 : form j k ts2) : @raxiom j k ts1 (untag f2) (subtract ts1 ts2 [::]) (equate f2).
proof: Proof. case: f2=>f2 [<- S A2]; case E : (subtract _ _ _)=>[rs1 rs2] A1; split=>//. case/(subtract_sound (sc_wf S A1) A2): E=>ys [/= D1 D2 D]. rewrite unitR in D1; apply: domeq_trans D1 _. rewrite domeq_sym; apply: domeq_trans D2 _. by rewrite domeq_sym; apply: domeqUn. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)