proposition: Lemma interp_perm i : forall t1 t2, perm t1 t2 -> interp i t1 = interp i t2.
proof: Proof. apply: perm_ind=>[s1 s2 ->-> //|t1 t2 x t1' t2' ->->|x y t1' t2' t ->->|x y t]. - by rewrite 2!interp_cons=>_ ->. - by rewrite !interp_cons unCA. by move=>_ -> _ ->. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)