diff --git a/SepCancel.v b/SepCancel.v
new file mode 100644
index 0000000..9949655
--- /dev/null
+++ b/SepCancel.v
@@ -0,0 +1,447 @@
+(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
+  * An entailment procedure for separation logic's assertion language
+  * Author: Adam Chlipala
+  * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
+
+Require Import Frap Setoid Classes.Morphisms.
+
+Set Implicit Arguments.
+
+Module Type SEP.
+  Parameter hprop : Type.
+  Parameter lift : Prop -> hprop.
+  Parameter star : hprop -> hprop -> hprop.
+  Parameter exis : forall A, (A -> hprop) -> hprop.
+
+  Notation "[| P |]" := (lift P).
+  Infix "*" := star.
+  Notation "'exists' x .. y , p" := (exis (fun x => .. (exis (fun y => p)) ..)).
+
+  Parameters himp heq : hprop -> hprop -> Prop.
+
+  Infix "===" := heq (no associativity, at level 70).
+  Infix "===>" := himp (no associativity, at level 70).
+
+  Axiom himp_heq : forall p q, p === q
+                               <-> (p ===> q /\ q ===> p).
+  Axiom himp_refl : forall p, p ===> p.
+  Axiom himp_trans : forall p q r, p ===> q -> q ===> r -> p ===> r.
+
+  Axiom lift_left : forall p (Q : Prop) r,
+    (Q -> p ===> r)
+    -> p * [| Q |] ===> r.
+  Axiom lift_right : forall p q (R : Prop),
+    R
+    -> p ===> q
+    -> p ===> q * [| R |].
+  Axiom extra_lift : forall (P : Prop) p,
+    P
+    -> p === [| P |] * p.
+
+  Axiom star_comm : forall p q, p * q === q * p.
+  Axiom star_assoc : forall p q r, p * (q * r) === (p * q) * r.
+  Axiom star_cancel : forall p1 p2 q1 q2, p1 ===> p2
+    -> q1 ===> q2
+    -> p1 * q1 ===> p2 * q2.
+
+  Axiom exis_gulp : forall A p (q : A -> _),
+    p * exis q === exis (fun x => p * q x).
+  Axiom exis_left : forall A (p : A -> _) q,
+    (forall x, p x ===> q)
+    -> exis p ===> q.
+  Axiom exis_right : forall A p (q : A -> _) x,
+    p ===> q x
+    -> p ===> exis q.
+End SEP.
+
+Module Make(Import S : SEP).
+  Add Parametric Relation : hprop himp
+    reflexivity proved by himp_refl
+    transitivity proved by himp_trans
+    as himp_rel.
+
+  Lemma heq_refl : forall p, p === p.
+  Proof.
+    intros; apply himp_heq; intuition (apply himp_refl).
+  Qed.
+
+  Lemma heq_sym : forall p q, p === q -> q === p.
+  Proof.
+    intros; apply himp_heq; apply himp_heq in H; intuition.
+  Qed.
+
+  Lemma heq_trans : forall p q r, p === q -> q === r -> p === r.
+  Proof.
+    intros; apply himp_heq; apply himp_heq in H; apply himp_heq in H0;
+    intuition (eauto using himp_trans).
+  Qed.
+
+  Add Parametric Relation : hprop heq
+    reflexivity proved by heq_refl
+    symmetry proved by heq_sym
+    transitivity proved by heq_trans
+    as heq_rel.
+
+  Instance himp_heq_mor : Proper (heq ==> heq ==> iff) himp.
+  Proof.
+    hnf; intros; hnf; intros.
+    apply himp_heq in H; apply himp_heq in H0.
+    intuition eauto using himp_trans.
+  Qed.
+
+  Add Parametric Morphism : star
+  with signature heq ==> heq ==> heq
+  as star_mor.
+  Proof.
+    intros; apply himp_heq; apply himp_heq in H; apply himp_heq in H0;
+    intuition (auto using star_cancel).
+  Qed.
+
+  Add Parametric Morphism : star
+  with signature himp ==> himp ==> himp
+  as star_mor'.
+  Proof.
+    auto using star_cancel.
+  Qed.
+
+  Instance exis_iff_morphism (A : Type) :
+    Proper (pointwise_relation A heq ==> heq) (@exis A).
+  Proof.
+    hnf; intros; apply himp_heq; intuition.
+    hnf in H.
+    apply exis_left; intro.
+    eapply exis_right.
+    assert (x x0 === y x0) by eauto.
+    apply himp_heq in H0; intuition eauto.
+    hnf in H.
+    apply exis_left; intro.
+    eapply exis_right.
+    assert (x x0 === y x0) by eauto.
+    apply himp_heq in H0; intuition eauto.
+  Qed.
+
+  Instance exis_imp_morphism (A : Type) :
+    Proper (pointwise_relation A himp ==> himp) (@exis A).
+  Proof.
+    hnf; intros.
+    apply exis_left; intro.
+    eapply exis_right.
+    unfold pointwise_relation in H.
+    eauto.
+  Qed.
+
+  Lemma star_combine_lift1 : forall P Q, [| P |] * [| Q |] ===> [| P /\ Q |].
+  Proof.
+    intros.
+    apply lift_left; intro.
+    rewrite extra_lift with (P := True); auto.
+    apply lift_left; intro.
+    rewrite extra_lift with (P := True) (p := [| P /\ Q |]); auto.
+    apply lift_right.
+    tauto.
+    reflexivity.
+  Qed.
+
+  Lemma star_combine_lift2 : forall P Q, [| P /\ Q |] ===> [| P |] * [| Q |].
+  Proof.
+    intros.
+    rewrite extra_lift with (P := True); auto.
+    apply lift_left; intro.
+    apply lift_right; try tauto.
+    rewrite extra_lift with (P := True) (p := [| P |]); auto.
+    apply lift_right; try tauto.
+    reflexivity.
+  Qed.
+
+  Lemma star_combine_lift : forall P Q, [| P |] * [| Q |] === [| P /\ Q |].
+  Proof.
+    intros.
+    apply himp_heq; auto using star_combine_lift1, star_combine_lift2.
+  Qed.
+
+  Lemma star_comm_lift : forall P q, [| P |] * q === q * [| P |].
+  Proof.
+    intros; apply star_comm.
+  Qed.
+
+  Lemma star_assoc_lift : forall p Q r,
+    (p * [| Q |]) * r === p * r * [| Q |].
+  Proof.
+    intros.
+    rewrite <- star_assoc.
+    rewrite (star_comm [| Q |]).
+    apply star_assoc.
+  Qed.
+
+  Lemma star_comm_exis : forall A (p : A -> _) q, exis p * q === q * exis p.
+  Proof.
+    intros; apply star_comm.
+  Qed.
+
+  Ltac lift :=
+    intros; apply himp_heq; split;
+    repeat (apply lift_left; intro);
+    repeat (apply lift_right; intuition).
+
+  Lemma lift_combine : forall p Q R,
+    p * [| Q |] * [| R |] === p * [| Q /\ R |].
+  Proof.
+    intros; apply himp_heq; split;
+    repeat (apply lift_left; intro);
+    repeat (apply lift_right; intuition).
+  Qed.
+
+  Lemma lift1_left : forall (P : Prop) q,
+    (P -> [| True |] ===> q)
+    -> [| P |] ===> q.
+  Proof.
+    intros.
+    rewrite (@extra_lift True [| P |]); auto.
+    apply lift_left; auto.
+  Qed.
+
+  Lemma lift1_right : forall p (Q : Prop),
+    Q
+    -> p ===> [| True |]
+    -> p ===> [| Q |].
+  Proof.
+    intros.
+    rewrite (@extra_lift True [| Q |]); auto.
+    apply lift_right; auto.
+  Qed.
+
+  Ltac normalize0 :=
+    setoid_rewrite exis_gulp
+    || setoid_rewrite lift_combine
+    || setoid_rewrite star_assoc
+    || setoid_rewrite star_combine_lift
+    || setoid_rewrite star_comm_lift
+    || setoid_rewrite star_assoc_lift
+    || setoid_rewrite star_comm_exis.
+
+  Ltac normalizeL :=
+    (apply exis_left || apply lift_left; intro; try congruence)
+    || match goal with
+         | [ |- lift ?P ===> _ ] =>
+           match P with
+             | True => fail 1
+             | _ => apply lift1_left; intro; try congruence
+           end
+       end.
+
+  Ltac normalizeR :=
+    match goal with
+    | [ |- _ ===> exis _ ] => eapply exis_right
+    | [ |- _ ===> _ * lift _ ] => apply lift_right
+    | [ |- _ ===> lift ?Q ] =>
+      match Q with
+      | True => fail 1
+      | _ => apply lift1_right
+      end
+    end.
+
+  Ltac normalize1 := normalize0 || normalizeL || normalizeR.
+
+  Lemma lift_uncombine : forall p P Q,
+    p * [| P /\ Q |] === p * [| P |] * [| Q |].
+  Proof.
+    lift.
+  Qed.
+  
+  Ltac normalize2 := setoid_rewrite lift_uncombine
+    || setoid_rewrite star_assoc.
+
+  Ltac normalizeLeft :=
+    let s := fresh "s" in intro s;
+    let rhs := fresh "rhs" in
+    match goal with
+      | [ |- _ ===> ?Q ] => set (rhs := Q)
+    end;
+    simpl; intros; repeat (normalize0 || normalizeL);
+    repeat match goal with
+             | [ H : ex _ |- _ ===> _ ] => destruct H
+             | [ H : _ /\ _ |- _ ] => destruct H
+             | [ H : _ = _ |- _ ] => rewrite H
+           end; subst rhs.
+                                                      
+  Ltac normalize :=
+    simpl; intros; repeat normalize1; repeat normalize2;
+    repeat (match goal with
+              | [ H : ex _ |- _ ===> _ ] => destruct H
+            end; intuition idtac).
+
+  Ltac forAllAtoms p k :=
+    match p with
+      | ?q * ?r => (forAllAtoms q k || forAllAtoms r k) || fail 2
+      | _ => k p
+    end.
+
+  Lemma stb1 : forall p q r,
+    (q * p) * r === q * r * p.
+  Proof.
+    intros; rewrite <- star_assoc; rewrite (star_comm p r); apply star_assoc.
+  Qed.
+
+  Ltac sendToBack part :=
+    repeat match goal with
+             | [ |- context[(?p * part) * ?q] ] => setoid_rewrite (stb1 part p q)
+             | [ |- context[part * ?p] ] => setoid_rewrite (star_comm part p)
+           end.
+
+  Theorem star_cancel' : forall p1 p2 q, p1 ===> p2
+    -> p1 * q ===> p2 * q.
+  Proof.
+    intros; apply star_cancel; auto using himp_refl.
+  Qed.
+
+  Theorem star_cancel'' : forall p q, lift True ===> q
+    -> p ===> p * q.
+  Proof.
+    intros.
+    eapply himp_trans.
+    rewrite extra_lift with (P := True); auto.
+    instantiate (1 := p * q).
+    rewrite star_comm.
+    apply star_cancel; auto.
+    reflexivity.
+    reflexivity.
+  Qed.
+
+  Ltac cancel1 :=
+    match goal with
+      | [ |- _ ===> ?Q ] =>
+        match Q with
+        | _ => is_evar Q; fail 1
+        | ?Q _ => is_evar Q; fail 1
+        | _ => apply himp_refl
+        end
+      | [ |- ?p ===> ?q ] =>
+        forAllAtoms p ltac:(fun p0 =>
+          sendToBack p0;
+          forAllAtoms q ltac:(fun q0 =>
+            sendToBack q0;
+            apply star_cancel'))
+      | _ => progress autorewrite with core
+    end.
+
+  Ltac hide_evars :=
+    repeat match goal with
+           | [ |- ?P ===> _ ] => is_evar P; set P
+           | [ |- _ ===> ?Q ] => is_evar Q; set Q
+           | [ |- context[star ?P _] ] => is_evar P; set P
+           | [ |- context[star _ ?Q] ] => is_evar Q; set Q
+           | [ |- _ ===> (exists v, _ * ?R v) ] => is_evar R; set R
+           end.
+
+  Ltac restore_evars :=
+    repeat match goal with
+           | [ x := _ |- _ ] => subst x
+           end.
+
+  Fixpoint flattenAnds (Ps : list Prop) : Prop :=
+    match Ps with
+    | nil => True
+    | [P] => P
+    | P :: Ps => P /\ flattenAnds Ps
+    end.
+
+  Ltac allPuresFrom k :=
+    match goal with
+    | [ H : ?P |- _ ] =>
+      match type of P with
+      | Prop => generalize dependent H; allPuresFrom ltac:(fun Ps => k (P :: Ps))
+      end
+    | _ => intros; k (@nil Prop)
+    end.
+
+  Ltac whichToQuantify skip foundAlready k :=
+    match goal with
+    | [ x : ?T |- _ ] =>
+      match type of T with
+      | Prop => fail 1
+      | _ =>
+        match skip with
+        | context[x] => fail 1
+        | _ =>
+          match foundAlready with
+          | context[x] => fail 1
+          | _ => (instantiate (1 := lift (x = x)); fail 2)
+                 || (instantiate (1 := fun _ => lift (x = x)); fail 2)
+                 || (whichToQuantify skip (x, foundAlready) k)
+          end
+        end
+      end
+    | _ => k foundAlready
+    end.
+
+  Ltac quantifyOverThem vars e k :=
+    match vars with
+    | tt => k e
+    | (?x, ?vars') =>
+      match e with
+      | context[x] =>
+        match eval pattern x in e with
+        | ?f _ => quantifyOverThem vars' (exis f) k
+        end
+      | _ => quantifyOverThem vars' e k
+      end
+    end.
+
+  Ltac addQuantifiers P k :=
+    whichToQuantify tt tt ltac:(fun vars =>
+        quantifyOverThem vars P k).
+
+  Ltac addQuantifiersSkipping x P k :=
+    whichToQuantify x tt ltac:(fun vars =>
+        quantifyOverThem vars P k).
+
+  Ltac basic_cancel :=
+    normalize; repeat cancel1; intuition eassumption.
+
+  Ltac cancel := hide_evars; normalize; repeat cancel1; restore_evars;
+                 repeat match goal with
+                        | [ H : True |- _ ] => clear H
+                        end;
+                 try match goal with
+                     | [ |- _ ===> ?p * ?q ] =>
+                       ((is_evar p; fail 1) || apply star_cancel'')
+                       || ((is_evar q; fail 1) || (rewrite (star_comm p q); apply star_cancel''))
+                     end;
+                 try match goal with
+                     | [ |- ?P ===> _ ] => sendToBack P;
+                       match goal with
+                       | [ |- ?P ===> ?Q * ?P ] => is_evar Q;
+                         rewrite (star_comm Q P);
+                         allPuresFrom ltac:(fun Ps =>
+                                              match Ps with
+                                              | nil => instantiate (1 := lift True)
+                                              | _ =>
+                                                let Ps' := eval simpl in (flattenAnds Ps) in
+                                                addQuantifiers (lift Ps') ltac:(fun e => instantiate (1 := e))
+                                              end;
+                                              basic_cancel)
+                       end
+                     | [ |- ?P ===> ?Q ] => is_evar Q;
+                       allPuresFrom ltac:(fun Ps =>
+                                            match Ps with
+                                            | nil => reflexivity
+                                            | _ =>
+                                              let Ps' := eval simpl in (flattenAnds Ps) in
+                                              addQuantifiers (star P (lift Ps')) ltac:(fun e => instantiate (1 := e));
+                                              basic_cancel
+                                            end)
+                     | [ |- ?P ===> ?Q ?x ] => is_evar Q;
+                        allPuresFrom ltac:(fun Ps =>
+                                             match Ps with
+                                             | nil => reflexivity
+                                             | _ =>
+                                               let Ps' := eval simpl in (flattenAnds Ps) in
+                                               addQuantifiersSkipping x (star P (lift Ps'))
+                                                 ltac:(fun e => match eval pattern x in e with
+                                                                | ?f _ => instantiate (1 := f)
+                                                                end);
+                                               basic_cancel
+                                             end)
+                     | [ |- _ ===> _ ] => intuition (try congruence)
+                     end; intuition (try eassumption).
+End Make.
diff --git a/SeparationLogic.v b/SeparationLogic.v
index 0ebdbf4..6a2eb68 100644
--- a/SeparationLogic.v
+++ b/SeparationLogic.v
@@ -3,7 +3,7 @@
   * Author: Adam Chlipala
   * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
 
-Require Import Frap Setoid Classes.Morphisms.
+Require Import Frap Setoid Classes.Morphisms SepCancel.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
@@ -92,448 +92,6 @@ Definition trsys_of (h : heap) {result} (c : cmd result) := {|
   Step := step (A := result)
 |}.
 
-
-(* CODE TO BE MOVED TO A LIBRARY MODULE SOON *)
-Module Type SEP.
-  Parameter hprop : Type.
-  Parameter lift : Prop -> hprop.
-  Parameter star : hprop -> hprop -> hprop.
-  Parameter exis : forall A, (A -> hprop) -> hprop.
-
-  Notation "[| P |]" := (lift P).
-  Infix "*" := star.
-  Notation "'exists' x .. y , p" := (exis (fun x => .. (exis (fun y => p)) ..)).
-
-  Parameters himp heq : hprop -> hprop -> Prop.
-
-  Infix "===" := heq (no associativity, at level 70).
-  Infix "===>" := himp (no associativity, at level 70).
-
-  Axiom himp_heq : forall p q, p === q
-                               <-> (p ===> q /\ q ===> p).
-  Axiom himp_refl : forall p, p ===> p.
-  Axiom himp_trans : forall p q r, p ===> q -> q ===> r -> p ===> r.
-
-  Axiom lift_left : forall p (Q : Prop) r,
-    (Q -> p ===> r)
-    -> p * [| Q |] ===> r.
-  Axiom lift_right : forall p q (R : Prop),
-    R
-    -> p ===> q
-    -> p ===> q * [| R |].
-  Axiom extra_lift : forall (P : Prop) p,
-    P
-    -> p === [| P |] * p.
-
-  Axiom star_comm : forall p q, p * q === q * p.
-  Axiom star_assoc : forall p q r, p * (q * r) === (p * q) * r.
-  Axiom star_cancel : forall p1 p2 q1 q2, p1 ===> p2
-    -> q1 ===> q2
-    -> p1 * q1 ===> p2 * q2.
-
-  Axiom exis_gulp : forall A p (q : A -> _),
-    p * exis q === exis (fun x => p * q x).
-  Axiom exis_left : forall A (p : A -> _) q,
-    (forall x, p x ===> q)
-    -> exis p ===> q.
-  Axiom exis_right : forall A p (q : A -> _) x,
-    p ===> q x
-    -> p ===> exis q.
-End SEP.
-
-Module Sep(Import S : SEP).
-  Add Parametric Relation : hprop himp
-    reflexivity proved by himp_refl
-    transitivity proved by himp_trans
-    as himp_rel.
-
-  Lemma heq_refl : forall p, p === p.
-  Proof.
-    intros; apply himp_heq; intuition (apply himp_refl).
-  Qed.
-
-  Lemma heq_sym : forall p q, p === q -> q === p.
-  Proof.
-    intros; apply himp_heq; apply himp_heq in H; intuition.
-  Qed.
-
-  Lemma heq_trans : forall p q r, p === q -> q === r -> p === r.
-  Proof.
-    intros; apply himp_heq; apply himp_heq in H; apply himp_heq in H0;
-    intuition (eauto using himp_trans).
-  Qed.
-
-  Add Parametric Relation : hprop heq
-    reflexivity proved by heq_refl
-    symmetry proved by heq_sym
-    transitivity proved by heq_trans
-    as heq_rel.
-
-  Instance himp_heq_mor : Proper (heq ==> heq ==> iff) himp.
-  Proof.
-    hnf; intros; hnf; intros.
-    apply himp_heq in H; apply himp_heq in H0.
-    intuition eauto using himp_trans.
-  Qed.
-
-  Add Parametric Morphism : star
-  with signature heq ==> heq ==> heq
-  as star_mor.
-  Proof.
-    intros; apply himp_heq; apply himp_heq in H; apply himp_heq in H0;
-    intuition (auto using star_cancel).
-  Qed.
-
-  Add Parametric Morphism : star
-  with signature himp ==> himp ==> himp
-  as star_mor'.
-  Proof.
-    auto using star_cancel.
-  Qed.
-
-  Instance exis_iff_morphism (A : Type) :
-    Proper (pointwise_relation A heq ==> heq) (@exis A).
-  Proof.
-    hnf; intros; apply himp_heq; intuition.
-    hnf in H.
-    apply exis_left; intro.
-    eapply exis_right.
-    assert (x x0 === y x0) by eauto.
-    apply himp_heq in H0; intuition eauto.
-    hnf in H.
-    apply exis_left; intro.
-    eapply exis_right.
-    assert (x x0 === y x0) by eauto.
-    apply himp_heq in H0; intuition eauto.
-  Qed.
-
-  Instance exis_imp_morphism (A : Type) :
-    Proper (pointwise_relation A himp ==> himp) (@exis A).
-  Proof.
-    hnf; intros.
-    apply exis_left; intro.
-    eapply exis_right.
-    unfold pointwise_relation in H.
-    eauto.
-  Qed.
-
-  Lemma star_combine_lift1 : forall P Q, [| P |] * [| Q |] ===> [| P /\ Q |].
-  Proof.
-    intros.
-    apply lift_left; intro.
-    rewrite extra_lift with (P := True); auto.
-    apply lift_left; intro.
-    rewrite extra_lift with (P := True) (p := [| P /\ Q |]); auto.
-    apply lift_right.
-    tauto.
-    reflexivity.
-  Qed.
-
-  Lemma star_combine_lift2 : forall P Q, [| P /\ Q |] ===> [| P |] * [| Q |].
-  Proof.
-    intros.
-    rewrite extra_lift with (P := True); auto.
-    apply lift_left; intro.
-    apply lift_right; try tauto.
-    rewrite extra_lift with (P := True) (p := [| P |]); auto.
-    apply lift_right; try tauto.
-    reflexivity.
-  Qed.
-
-  Lemma star_combine_lift : forall P Q, [| P |] * [| Q |] === [| P /\ Q |].
-  Proof.
-    intros.
-    apply himp_heq; auto using star_combine_lift1, star_combine_lift2.
-  Qed.
-
-  Lemma star_comm_lift : forall P q, [| P |] * q === q * [| P |].
-  Proof.
-    intros; apply star_comm.
-  Qed.
-
-  Lemma star_assoc_lift : forall p Q r,
-    (p * [| Q |]) * r === p * r * [| Q |].
-  Proof.
-    intros.
-    rewrite <- star_assoc.
-    rewrite (star_comm [| Q |]).
-    apply star_assoc.
-  Qed.
-
-  Lemma star_comm_exis : forall A (p : A -> _) q, exis p * q === q * exis p.
-  Proof.
-    intros; apply star_comm.
-  Qed.
-
-  Ltac lift :=
-    intros; apply himp_heq; split;
-    repeat (apply lift_left; intro);
-    repeat (apply lift_right; intuition).
-
-  Lemma lift_combine : forall p Q R,
-    p * [| Q |] * [| R |] === p * [| Q /\ R |].
-  Proof.
-    intros; apply himp_heq; split;
-    repeat (apply lift_left; intro);
-    repeat (apply lift_right; intuition).
-  Qed.
-
-  Lemma lift1_left : forall (P : Prop) q,
-    (P -> [| True |] ===> q)
-    -> [| P |] ===> q.
-  Proof.
-    intros.
-    rewrite (@extra_lift True [| P |]); auto.
-    apply lift_left; auto.
-  Qed.
-
-  Lemma lift1_right : forall p (Q : Prop),
-    Q
-    -> p ===> [| True |]
-    -> p ===> [| Q |].
-  Proof.
-    intros.
-    rewrite (@extra_lift True [| Q |]); auto.
-    apply lift_right; auto.
-  Qed.
-
-  Ltac normalize0 :=
-    setoid_rewrite exis_gulp
-    || setoid_rewrite lift_combine
-    || setoid_rewrite star_assoc
-    || setoid_rewrite star_combine_lift
-    || setoid_rewrite star_comm_lift
-    || setoid_rewrite star_assoc_lift
-    || setoid_rewrite star_comm_exis.
-
-  Ltac normalizeL :=
-    (apply exis_left || apply lift_left; intro; try congruence)
-    || match goal with
-         | [ |- lift ?P ===> _ ] =>
-           match P with
-             | True => fail 1
-             | _ => apply lift1_left; intro; try congruence
-           end
-       end.
-
-  Ltac normalizeR :=
-    match goal with
-    | [ |- _ ===> exis _ ] => eapply exis_right
-    | [ |- _ ===> _ * lift _ ] => apply lift_right
-    | [ |- _ ===> lift ?Q ] =>
-      match Q with
-      | True => fail 1
-      | _ => apply lift1_right
-      end
-    end.
-
-  Ltac normalize1 := normalize0 || normalizeL || normalizeR.
-
-  Lemma lift_uncombine : forall p P Q,
-    p * [| P /\ Q |] === p * [| P |] * [| Q |].
-  Proof.
-    lift.
-  Qed.
-  
-  Ltac normalize2 := setoid_rewrite lift_uncombine
-    || setoid_rewrite star_assoc.
-
-  Ltac normalizeLeft :=
-    let s := fresh "s" in intro s;
-    let rhs := fresh "rhs" in
-    match goal with
-      | [ |- _ ===> ?Q ] => set (rhs := Q)
-    end;
-    simpl; intros; repeat (normalize0 || normalizeL);
-    repeat match goal with
-             | [ H : ex _ |- _ ===> _ ] => destruct H
-             | [ H : _ /\ _ |- _ ] => destruct H
-             | [ H : _ = _ |- _ ] => rewrite H
-           end; subst rhs.
-                                                      
-  Ltac normalize :=
-    simpl; intros; repeat normalize1; repeat normalize2;
-    repeat (match goal with
-              | [ H : ex _ |- _ ===> _ ] => destruct H
-            end; intuition idtac).
-
-  Ltac forAllAtoms p k :=
-    match p with
-      | ?q * ?r => (forAllAtoms q k || forAllAtoms r k) || fail 2
-      | _ => k p
-    end.
-
-  Lemma stb1 : forall p q r,
-    (q * p) * r === q * r * p.
-  Proof.
-    intros; rewrite <- star_assoc; rewrite (star_comm p r); apply star_assoc.
-  Qed.
-
-  Ltac sendToBack part :=
-    repeat match goal with
-             | [ |- context[(?p * part) * ?q] ] => setoid_rewrite (stb1 part p q)
-             | [ |- context[part * ?p] ] => setoid_rewrite (star_comm part p)
-           end.
-
-  Theorem star_cancel' : forall p1 p2 q, p1 ===> p2
-    -> p1 * q ===> p2 * q.
-  Proof.
-    intros; apply star_cancel; auto using himp_refl.
-  Qed.
-
-  Theorem star_cancel'' : forall p q, lift True ===> q
-    -> p ===> p * q.
-  Proof.
-    intros.
-    eapply himp_trans.
-    rewrite extra_lift with (P := True); auto.
-    instantiate (1 := p * q).
-    rewrite star_comm.
-    apply star_cancel; auto.
-    reflexivity.
-    reflexivity.
-  Qed.
-
-  Ltac cancel1 :=
-    match goal with
-      | [ |- _ ===> ?Q ] =>
-        match Q with
-        | _ => is_evar Q; fail 1
-        | ?Q _ => is_evar Q; fail 1
-        | _ => apply himp_refl
-        end
-      | [ |- ?p ===> ?q ] =>
-        forAllAtoms p ltac:(fun p0 =>
-          sendToBack p0;
-          forAllAtoms q ltac:(fun q0 =>
-            sendToBack q0;
-            apply star_cancel'))
-      | _ => progress autorewrite with core
-    end.
-
-  Ltac hide_evars :=
-    repeat match goal with
-           | [ |- ?P ===> _ ] => is_evar P; set P
-           | [ |- _ ===> ?Q ] => is_evar Q; set Q
-           | [ |- context[star ?P _] ] => is_evar P; set P
-           | [ |- context[star _ ?Q] ] => is_evar Q; set Q
-           | [ |- _ ===> (exists v, _ * ?R v) ] => is_evar R; set R
-           end.
-
-  Ltac restore_evars :=
-    repeat match goal with
-           | [ x := _ |- _ ] => subst x
-           end.
-
-  Fixpoint flattenAnds (Ps : list Prop) : Prop :=
-    match Ps with
-    | nil => True
-    | [P] => P
-    | P :: Ps => P /\ flattenAnds Ps
-    end.
-
-  Ltac allPuresFrom k :=
-    match goal with
-    | [ H : ?P |- _ ] =>
-      match type of P with
-      | Prop => generalize dependent H; allPuresFrom ltac:(fun Ps => k (P :: Ps))
-      end
-    | _ => intros; k (@nil Prop)
-    end.
-
-  Ltac whichToQuantify skip foundAlready k :=
-    match goal with
-    | [ x : ?T |- _ ] =>
-      match type of T with
-      | Prop => fail 1
-      | _ =>
-        match skip with
-        | context[x] => fail 1
-        | _ =>
-          match foundAlready with
-          | context[x] => fail 1
-          | _ => (instantiate (1 := lift (x = x)); fail 2)
-                 || (instantiate (1 := fun _ => lift (x = x)); fail 2)
-                 || (whichToQuantify skip (x, foundAlready) k)
-          end
-        end
-      end
-    | _ => k foundAlready
-    end.
-
-  Ltac quantifyOverThem vars e k :=
-    match vars with
-    | tt => k e
-    | (?x, ?vars') =>
-      match e with
-      | context[x] =>
-        match eval pattern x in e with
-        | ?f _ => quantifyOverThem vars' (exis f) k
-        end
-      | _ => quantifyOverThem vars' e k
-      end
-    end.
-
-  Ltac addQuantifiers P k :=
-    whichToQuantify tt tt ltac:(fun vars =>
-        quantifyOverThem vars P k).
-
-  Ltac addQuantifiersSkipping x P k :=
-    whichToQuantify x tt ltac:(fun vars =>
-        quantifyOverThem vars P k).
-
-  Ltac basic_cancel :=
-    normalize; repeat cancel1; intuition eassumption.
-
-  Ltac cancel := hide_evars; normalize; repeat cancel1; restore_evars;
-                 repeat match goal with
-                        | [ H : True |- _ ] => clear H
-                        end;
-                 try match goal with
-                     | [ |- _ ===> ?p * ?q ] =>
-                       ((is_evar p; fail 1) || apply star_cancel'')
-                       || ((is_evar q; fail 1) || (rewrite (star_comm p q); apply star_cancel''))
-                     end;
-                 try match goal with
-                     | [ |- ?P ===> _ ] => sendToBack P;
-                       match goal with
-                       | [ |- ?P ===> ?Q * ?P ] => is_evar Q;
-                         rewrite (star_comm Q P);
-                         allPuresFrom ltac:(fun Ps =>
-                                              match Ps with
-                                              | nil => instantiate (1 := lift True)
-                                              | _ =>
-                                                let Ps' := eval simpl in (flattenAnds Ps) in
-                                                addQuantifiers (lift Ps') ltac:(fun e => instantiate (1 := e))
-                                              end;
-                                              basic_cancel)
-                       end
-                     | [ |- ?P ===> ?Q ] => is_evar Q;
-                       allPuresFrom ltac:(fun Ps =>
-                                            match Ps with
-                                            | nil => reflexivity
-                                            | _ =>
-                                              let Ps' := eval simpl in (flattenAnds Ps) in
-                                              addQuantifiers (star P (lift Ps')) ltac:(fun e => instantiate (1 := e));
-                                              basic_cancel
-                                            end)
-                     | [ |- ?P ===> ?Q ?x ] => is_evar Q;
-                        allPuresFrom ltac:(fun Ps =>
-                                             match Ps with
-                                             | nil => reflexivity
-                                             | _ =>
-                                               let Ps' := eval simpl in (flattenAnds Ps) in
-                                               addQuantifiersSkipping x (star P (lift Ps'))
-                                                 ltac:(fun e => match eval pattern x in e with
-                                                                | ?f _ => instantiate (1 := f)
-                                                                end);
-                                               basic_cancel
-                                             end)
-                     | [ |- _ ===> _ ] => intuition (try congruence)
-                     end; intuition (try eassumption).
-End Sep.
-
-
 (* Now we instantiate the generic signature of separation-logic assertions and
  * connectives. *)
 Module Import S <: SEP.
@@ -671,8 +229,7 @@ End S.
 
 Export S.
 (* Instantiate our big automation engine to these definitions. *)
-Module Import Se := Sep(S).
-Export Se.
+Module Import Se := SepCancel.Make(S).
 
 
 (* ** Some extra predicates outside the set that the engine knows about *)
diff --git a/_CoqProject b/_CoqProject
index 8424197..0746574 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -24,4 +24,5 @@ LambdaCalculusAndTypeSoundness.v
 TypesAndMutation.v
 DeepAndShallowEmbeddings_template.v
 DeepAndShallowEmbeddings.v
+SepCancel.v
 SeparationLogic.v