proposition: Lemma subterm_sound i ts1 ts2 : all (wf i) ts1 -> all (wf i) ts2 -> subterm ts1 ts2 -> exists u, dom_eq (interp i ts1 \+ u) (interp i ts2).
proof: Proof. elim: ts1 ts2=>[|t ts1 IH] ts2 /= A1 A2. - by exists (interp i ts2); rewrite unitL. case/andP: A1; case: t=>[n v|n] /= /size_onth [k] X A1; rewrite X; case: ifP=>Y //. - case: (keyP Y X)=>w -> /(IH _ A1 (wf_kfree n A2)) [xs D]. by exists xs; rewrite -joinA; apply: domeqUn D. move: (varP Y X)=>-> /(IH _ A1 (wf_vfree n A2)) [xs D]. by exists xs; rewrite -joinA; apply: domeqUn D. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)