proposition: Lemma subtract_sound i ts1 ts2 rs1 xs : all (wf i) ts1 -> all (wf i) ts2 -> subtract ts1 ts2 xs = Some rs1 -> interp i ts1 \+ interp i xs = interp i rs1 \+ interp i ts2.
proof: Proof. elim: ts1 ts2 xs=>[|t ts1 IH] ts2 xs /= =>[_|/andP [At A1]]. - by case: ts2=>//=_; case=>->; rewrite unitR unitL. case: t At=>n /= /size_onth [x X] A2; case: ifP=>Y. - rewrite -joinA; move: (expP i Y)=>-> /(IH _ _ A1 (wf_efree n A2))->. by rewrite joinCA. by move/(IH _ _ A1 A2)=><-/=; rewrite joinCA joinA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm)