proposition: Lemma cancel_sound i t1 t2 : def (interp i t1) -> interp i t1 = interp i t2 -> eval i (cancel i t1 t2).
proof: Proof. by move=>D H; apply: cancel_sound'=>//; rewrite -H // cats0. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)