fact: Fixpoint cancel' (i : ctx) (t1 t2 r : synheap) (f : seq fact) : seq fact := match t1 with | [::] => match r, t2 with | [::], [::] => f | [:: Pts x d], [:: Pts x' d'] => [:: eqX x x', eqD d d' & f] | _ , _ => [:: eqH r t2 & f] end | Pts x d :: t1' => if x \in ptrs t2 then cancel' i t1' (pfree x t2) r [:: eqD d (pread' x t2) & f] else cancel' i t1' t2 [:: Pts x d & r] f | Var h :: t1' => if h \in vars t2 then cancel' i t1' (hfree h t2) r f else cancel' i t1' t2 [:: Var h & r] f end.
imports: mathcomp(ssreflect ssrbool ssrnat ssrfun eqtype seq) LemmaOverloading(prelude prefix perms heaps)