proposition: Lemma subtract_sound i ts1 ts2 rs1 rs2 xs : all (wf i) ts1 -> all (wf i) ts2 -> subtract ts1 ts2 xs = (rs1, rs2) -> exists u, dom_eq (interp i ts1 \+ interp i xs) (interp i rs1 \+ u) /\ dom_eq (interp i ts2) (interp i rs2 \+ u).
proof: Proof. elim: ts1 ts2 xs=>[|t ts1 IH] ts2 xs /= A1 A2. - by case=><-<-; exists Unit; rewrite unitL !unitR. case/andP: A1; case: t=>[n v|n] /= /size_onth [x X] A1; rewrite X; case: ifP=>Y. - case: (keyP Y X)=>w -> /(IH _ _ A1 (wf_kfree n A2)) [u][H1 H2]. exists (pts x v \+ u); rewrite -joinA !(pull (pts x _)). by split=>//; apply: domeqUn. - by case/(IH _ _ A1 A2)=>u [/= H1 H2]; rewrite X joinCA joinA in H1; exists u. - move: (varP Y X)=>-> /(IH _ _ A1 (wf_vfree n A2)) [u][H1 H2]. by exists (x \+ u); rewrite -joinA !(pull x); split=>//; apply: domeqUn. by case/(IH _ _ A1 A2)=>u [/= H1 H2]; rewrite X joinCA joinA in H1; exists u. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)