diff --git a/slot_mereology.v b/slot_mereology.v
index b8994681825586d82dfe057f125535f7186ac255..e11479cf2af5ce618b9c7606d258b7002600d808 100644
--- a/slot_mereology.v
+++ b/slot_mereology.v
@@ -16,12 +16,12 @@ Definition Os x y := exists z, Ps z x /\ Ps z y.
 Definition PPs x y := Ps x y /\ ~ F y x.
 
 (* Only Slots are Filled *)
-Axiom only_slots_are_filled : forall x y,
-  F x y -> exists z, Ps y z.
+Axiom only_slots_are_filled : forall a s,
+  F a s -> exists b, Ps s b.
 
 (* Slots Cannot Fill *)
-Axiom slots_cannot_fill : forall x y,
-  F x y -> ~exists z, Ps x z.
+Axiom slots_cannot_fill : forall a s,
+  F a s -> ~exists b, Ps a b.
 
 (* Slots Don’t Have Slots *)
 Axiom slots_dont_have_slots : forall x y,
@@ -106,17 +106,17 @@ Axiom mutual_occupancy : forall x y z1 z2,
 Axiom single_occupancy : forall x y,
   Ps x y -> exists! z, F z x.
 
-(* Single Owner *)
-Lemma single_filler : forall s x,
-  F x s -> forall y, F y s -> x = y.
-Proof.
-  intros s x Fxs y Fys.
-  pose proof (only_slots_are_filled x s Fxs) as (z & Pssz).
-  pose proof (single_occupancy s z Pssz) as (z' & Fz's & UniqueFs).
-  apply UniqueFs in Fys as ->.
-  apply UniqueFs in Fxs.
-  auto.
-Qed.
+Ltac unify_filler F1 F2 :=
+  let a := fresh "a" in
+  let Pssa := fresh "Pssa" in
+  let UniqueF := fresh "UniqueF" in
+  let a' := fresh "a'" in
+  pose proof (only_slots_are_filled _ _ F2) as (a & Pssa);
+  pose proof (single_occupancy _ _ Pssa) as (a' & _ & UniqueF);
+  apply UniqueF in F1 as eq1;
+  apply UniqueF in F2 as eq2;
+  symmetry in eq2;
+  subst; clear a Pssa UniqueF F2.
 
 (* Parthood Transitivity *)
 Theorem parthood_transitivity : forall x y z,
@@ -182,9 +182,7 @@ Proof.
        pose proof (Uc a Fac). subst.
        pose proof (Uc b Fbc). subst.
        apply nPba.
-       exists c; split.
-       apply Fbc.
-       apply Pscb.
+       exists c; split; assumption.
   (* right to left *)
   - intros [a [Psab nFba]].
     pose proof (single_occupancy _ _ Psab) as [c [Fca Uc]].
@@ -201,10 +199,18 @@ Proof.
 Qed.
 
 (* Slot Strong Supplementation *)
-Axiom BA8 : forall x y,
-  (exists z, Ps z x) /\ (exists z, Ps z y) ->
-    ((~exists z, Ps z x /\ F y z) ->
-      (exists z, Ps z y /\ ~Ps z x)).
+Theorem BA8 : forall a b,
+  (exists s, Ps s a) /\ (exists t, Ps t b) ->
+    (~(exists u, Ps u a /\ F b u) ->
+      (exists v, Ps v b /\ ~Ps v a)).
+Proof.
+  intros a b ((s & Pssa) & (t & Pstb)) nPba.
+  pose proof (whole_improper_slots b (ex_intro _ t (Pstb))) as (u & Psub & Fbu).
+  exists u; split; auto.
+  intros Psua.
+  destruct nPba.
+  exists u; split; assumption.
+Qed.
 
 (* Slot Weak Supplementation *)
 Theorem BT13 : forall x y,
@@ -239,292 +245,330 @@ Abort.
  *                    *
  **********************)
 
-Definition S s := exists x, Ps s x.
+(*******************
+ * Slot Definition *
+ *******************)
+Definition S s := exists a, Ps s a.
+
+Axiom single_owner : forall a b s, Ps s a -> Ps s b -> a = b.
 
-(* Single Owner *)
-Axiom single_owner : forall s x,
-  Ps s x -> forall y, Ps s y -> x = y.
+Ltac unify_owner Ps1 Ps2 :=
+  pose proof (single_owner _ _ _ Ps2 Ps1);
+  subst; clear Ps2.
 
-(* Anti-Inheritance *)
-Theorem anti_inheritance : forall x y s t,
-  x <> y /\ Ps s y /\ F x s /\ Ps t x -> ~Ps t y.
+Theorem anti_inheritance : forall a b s t,
+  a <> b -> Ps s b -> F a s -> Ps t a -> ~Ps t b.
 Proof.
-  intros x y s t (x_neq_y & Pssy & Fxs & Pstx).
-  intro h.
-  apply x_neq_y.
-  apply single_owner with (s:=t); assumption.
+  intros a b s t a_neq_b Pssb Fas Psta h.
+  unify_owner Psta h.
+  contradiction.
 Qed.
 
-Definition IPs x y := Ps x y /\ F y x.
+Definition IPs s a := Ps s a /\ F a s.
 
-(* Slots are either proper or improper. *)
-Theorem either_proper_or_improper : forall s,
-  S s -> exists x, PPs s x /\ ~ IPs s x \/ ~ PPs s x /\ IPs s x.
+Lemma either_proper_or_improper : forall s,
+  S s -> exists a, PPs s a /\ ~ IPs s a \/ ~ PPs s a /\ IPs s a.
 Proof.
-  intros s [x Pssx].
-  exists x.
-  destruct (classic (F x s)) as [Fxs|NFxs].
-  - right.
-    split.
-    + intros [_ NFxs].
-      contradiction.
-    + split; assumption.
-  - left.
-    split.
-    + split; assumption.
-    + intros [_ Fxs].
-      contradiction.
+  intros s (a & Pssa); exists a.
+  destruct (classic (F a s)) as [Fas|NFas];
+  [right|left]; split.
+  - intros [_ NFxs]; contradiction.
+  - split; assumption.
+  - split; assumption.
+  - intros [_ Fxs]; contradiction.
 Qed.
 
-(* Improper Slots are only owned by their Filler *)
-Lemma unique_owner_improper_slot : forall x s,
-  IPs s x -> forall y, Ps s y -> x = y.
+Lemma proper_part_in_proper_slot : forall a b,
+  PP b a <-> (exists s, PPs s a /\ F b s).
 Proof.
-  intros x s [Pssx _].
-  apply single_owner.
-  assumption.
+  intros a b.
+  split.
+  - intros ((s & Fbs & Pssa) & nPab).
+    exists s; repeat split; auto.
+    intros Fas; destruct nPab.
+    unify_filler Fas Fbs.
+    apply BT9; exists s; assumption.
+  - intros (s & [Pssa nFas] & Fbs).
+    split.
+    exists s; split; auto.
+    intros Pab; destruct nFas.
+    assert (a = b) as <-.
+    apply BT8; split; auto.
+    split with (x:=s); split; auto.
+    assumption.
 Qed.
 
-(* *)
-Theorem proper_part_in_proper_slot : forall x y,
-  PP y x -> (exists s, Ps s x /\ F y s /\ ~Ps s y).
-Proof.
-  intros x y [[s [Fys Pssx]] nPxy].
-  exists s.
-  repeat split; try assumption.
-  intro Pssy.
-  destruct nPxy.
-  pose proof (single_owner s x Pssx) as UniqueSOwner.
-  apply UniqueSOwner in Pssy.
-  rewrite <- Pssy.
-  apply BT9.
-  exists s; assumption.
-Qed.
- 
-(* Additional Improper Parthood Slots *)
-Axiom filler_has_imp_slot : forall x s, F x s -> exists t, IPs t x.
+Axiom filler_has_imp_slot : forall a s, F a s -> exists t, IPs t a.
 
-(* General Conditional Reflexivity *)
-Lemma general_conditional_refl : forall x s,
-  Ps s x \/ F x s -> P x x.
+Lemma general_conditional_refl : forall a s,
+  Ps s a \/ F a s -> P a a.
 Proof.
-  intros x s Ps_or_F.
+  intros a s Ps_or_F.
   apply BT9.
-  destruct Ps_or_F as [Pssx|Fxs].
+  destruct Ps_or_F as [Pssa|Fas].
   - exists s; assumption.
-  - pose proof (filler_has_imp_slot x s Fxs) as (t & Pstx & _).
+  - pose proof (filler_has_imp_slot a s Fas) as (t & Psta & _).
     exists t; assumption.
 Qed.
 
 (* Only One Improper Slot per Filler *)
-Axiom unique_improper_slot : forall x s t,
-  IPs s x -> IPs t x -> s = t.
+Axiom unique_improper_slot : forall a s t,
+  IPs s a -> IPs t a -> s = t.
+
+Ltac unify_improper_slot IPs1 IPs2 :=
+  pose proof (unique_improper_slot _ _ _ IPs2 IPs1);
+  subst; clear IPs2.
 
-Theorem mutual_occupancy_is_slot_identity : forall s t x y,
-  Ps s y -> F x s -> Ps t x -> F y t -> s = t.
+Theorem mutual_occupancy_is_slot_identity : forall a b s t,
+  Ps s b -> F a s -> Ps t a -> F b t -> s = t.
 Proof.
-  intros s t x y Pssy Fxs Pstx Fyt.
-  pose proof (mutual_occupancy x y s t (conj (conj Pssy Fxs) (conj Pstx Fyt))) as <-.
-  apply unique_improper_slot with (x:=x); split; assumption.
+  intros a b s t Pssb Fas Psta Fbt.
+  pose proof (mutual_occupancy a b s t (conj (conj Pssb Fas) (conj Psta Fbt))) as <-.
+  apply unique_improper_slot with (a:=a); split; assumption.
 Qed.
 
-(***************
- * Composition *
- ***************)
+(*********************
+ * Contextualisation *
+ *********************)
 
 Parameter C : Entity -> Entity -> Entity -> Prop.
 
-Axiom compo_domains : forall u s t, C u s t -> S u /\ S s /\ S t.
+Axiom context_domains : forall u s t, C u s t -> S u /\ S s /\ S t.
 
-(* Composition Existence *)
-Axiom composition_existence : forall s t x,
-  F x s -> Ps t x -> exists u, C u s t.
+Definition Cb s t := exists a, F a t /\ Ps s a.
 
-Axiom composition_constraints : forall s t u,
-  C u s t -> exists x, F x s /\ Ps t x.
+Axiom context_existence : forall s t,
+  Cb t s -> exists u, C u s t.
 
-(* Composition Unicity *)
-Axiom composition_unicity : forall s t u v,
-  C u s t -> C v s t -> u = v.
+Axiom context_constraints : forall s t u,
+  C u s t -> Cb t s.
 
-Axiom compo_left_inject : forall s t u v,
-  C v s t -> C v s u -> t = u.
+Axiom context_unicity : forall s t u v,
+  C u s t -> C v s t -> u = v.
 
-Axiom compo_right_inject : forall s t u v x,
-  C v t s -> C v u s -> IPs s x -> t = u.
+Ltac unify_context C1 C2 :=
+  pose proof (context_unicity _ _ _ _ C2 C1);
+  subst; clear C2.
 
-Theorem symmetric_compositions_are_slot_identity :
+Theorem symmetric_context_are_slot_identity :
   forall s t u v, C u s t -> C v t s -> s = t.
 Proof.
   intros s t u v Cust Cvts.
-  pose proof (composition_constraints s t u Cust) as (x & Fxs & Pstx).
-  pose proof (composition_constraints t s v Cvts) as (y & Fyt & Pssy).
-  apply mutual_occupancy_is_slot_identity with (x:=x) (y:=y); assumption.
+  pose proof (context_constraints s t u Cust) as (a & Fas & Psta).
+  pose proof (context_constraints t s v Cvts) as (b & Fbt & Pssb).
+  apply mutual_occupancy_is_slot_identity with (a:=a) (b:=b); assumption.
 Qed.
 
-Axiom compo_asso_lr : forall a b c d e,
-  C a b c -> C b d e -> exists f, C a d f /\ C f e c.
+Axiom context_left_inject : forall s t u v,
+  C v s t -> C v s u -> t = u.
 
-Axiom compo_asso_rl : forall a c d e f,
-  C a d f -> C f e c -> exists b, C a b c /\ C b d e.
+Axiom context_right_inject : forall s t u v a,
+  C v t s -> C v u s -> IPs s a -> t = u.
 
-(* Composition Associativity *)
-Theorem compo_asso_eq : forall s t u a b c d,
-  (C a s t -> C b a u -> C d s c -> C c t u -> b = d).
-Proof.
-  intros s t u a b c d Cast Cbau Cdsc Cctu.
-  pose proof (compo_asso_lr b a u s t Cbau Cast) as (x & Cbsx & Cxtu).
-  pose proof (composition_unicity t u c x Cctu Cxtu) as <-.
-  apply composition_unicity with (s:=s) (t:=c); assumption.
-Qed.
+Axiom context_asso : forall s t u v,
+  (exists w, C v s w /\ C w t u) <-> (exists x, C v x u /\ C x s t).
+
+Ltac context_asso s := apply context_asso; exists s; auto.
 
-(* Improper-Improper Composition *)
+(* Improper-Improper Contextualisation *)
 (* v = s o s *)
 (* u = (s o s) o t *)
-Theorem imp_imp_composition : forall s a,
-  IPs s a -> C s s s.
-Proof.
-  intros s a (Pssa & Fas).
-  pose proof (composition_existence s s a Fas Pssa) as (v & Cvss).
-  pose proof (compo_domains v s s Cvss) as [(b & Psvb) _].
-  pose proof (single_occupancy v b Psvb) as (c & Fcv & _).
-  clear Psvb b.
-  (* Proof of a = c *)
-  pose proof (filler_has_imp_slot c v Fcv) as (t & Pstc & Fct).
-  pose proof (composition_existence v t c Fcv Pstc) as (u & Cuvt).
-  pose proof (compo_asso_lr u v t s s Cuvt Cvss) as (d & Cusd & Cdst).
-  pose proof (composition_constraints s t d Cdst) as (y & Fys & Psty).
-  pose proof (single_occupancy s a Pssa) as (z & Fzs & FsUnique).
-  apply FsUnique in Fas as ->, Fys as <-.
-  clear FsUnique.
-  pose proof (single_owner t a Psty) as PstUnique.
-  apply PstUnique in Pstc as <-.
-  clear PstUnique.
-  pose proof (unique_improper_slot a s t (conj Pssa Fzs) (conj Psty Fct)) as <-.
-  (* Proof of a = b *)
-  pose proof (compo_asso_lr u v s s s Cuvt Cvss) as (v' & Cusv' & Cv'ss).
-  pose proof (composition_unicity s s v v' Cvss Cv'ss) as <-.
-  pose proof (symmetric_compositions_are_slot_identity s v u u Cusv' Cuvt) as <-.
-  assumption.
-Qed.
-
-Theorem imp_imp_compo_rev : forall s,
-  C s s s -> exists x, IPs s x.
-Proof.
-  intros s Csss.
-  pose proof (composition_constraints s s s Csss) as (x & Fxs & Pssx).
-  exists x; split; assumption.
+Theorem imp_imp_context : forall s,
+  (exists a, IPs s a) <-> C s s s.
+Proof.
+  intros s; split.
+  + intros (a & Pssa & Fas).
+    pose proof (context_existence s s (ex_intro _ a (conj Fas Pssa))) as (v & Cvss).
+    pose proof (context_domains v s s Cvss) as [(b & Psvb) _].
+    pose proof (single_occupancy v b Psvb) as (c & Fcv & _).
+    clear Psvb b.
+    (* Proof of a = c *)
+    pose proof (filler_has_imp_slot c v Fcv) as (t & Pstc & Fct).
+    pose proof (context_existence v t (ex_intro _ _ (conj Fcv Pstc))) as (u & Cuvt).
+    assert (exists d, C u s d /\ C d s t) as (d & Cust & Cdst).
+    context_asso v.
+    pose proof (context_constraints s t d Cdst) as (y & Fys & Psty).
+    unify_filler Fas Fys.
+    unify_owner Psty Pstc.
+    pose proof (unique_improper_slot a s t (conj Pssa Fas) (conj Psty Fct)) as <-.
+    (* Proof of a = b *)
+    assert (exists v', C u s v' /\ C v' s s) as (v' & Cusv' & Cv'ss).
+    context_asso v.
+    unify_context Cvss Cv'ss.
+    pose proof (symmetric_context_are_slot_identity s v u u Cusv' Cuvt) as <-.
+    assumption.
+  + intros Csss.
+    pose proof (context_constraints _ _ _ Csss) as (a & Fas & Pssa).
+    exists a; split; auto.
 Qed.
 
 (* Proper-Improper Composition *)
-Theorem right_imp_composition : forall s t x,
-  IPs s x -> F x t -> C t t s.
+Theorem right_imp_composition : forall s t a,
+  IPs s a -> F a t -> C t t s.
 Proof.
   intros s t x (Pssx & Fxs) Fxt.
-  pose proof (imp_imp_composition s x (conj Pssx Fxs)) as Csss.
-  pose proof (composition_existence t s x Fxt Pssx) as (u & Cuts).
-  pose proof (compo_asso_rl u s t s s Cuts Csss) as (v & Cuvs & Cvts).
-  pose proof (composition_unicity t s u v Cuts Cvts) as <-.
-  pose proof (composition_constraints u s u Cuvs) as (y & Fyu & Pssy).
-  pose proof (single_owner s x Pssx y Pssy) as <-.
-  pose proof (compo_right_inject s t u u x Cuts Cuvs (conj Pssx Fxs)) as <-.
+  assert (Csss: C s s s). apply imp_imp_context; exists x; split; auto.
+  pose proof (context_existence t s (ex_intro _ _ (conj Fxt Pssx))) as (u & Cuts).
+  assert (exists v, C u v s /\ C v t s) as (v & Cuvs & Cvts). context_asso s.
+  unify_context Cuts Cvts.
+  pose proof (context_constraints u s u Cuvs) as (y & Fyu & Pssy).
+  unify_owner Pssx Pssy.
+  pose proof (context_right_inject s t u u x Cuts Cuvs (conj Pssx Fxs)) as <-.
   assumption.
 Qed.
 
 (* Improper-Proper Composition *)
-Theorem left_imp_composition : forall s t x,
-  IPs s x -> Ps t x -> C t s t.
+Theorem left_imp_composition : forall s t a,
+  IPs s a -> Ps t a -> C t s t.
 Proof.
   intros s t x (Pssx & Fxs) Pstx.
-  pose proof (imp_imp_composition s x (conj Pssx Fxs)) as Csss.
-  pose proof (composition_existence s t x Fxs Pstx) as (u & Cust).
-  pose proof (compo_asso_lr u s t s s Cust Csss) as (v & Cusv & Cvst).
-  pose proof (composition_unicity s t u v Cust Cvst) as <-.
-  pose proof (compo_left_inject s t u u Cust Cusv) as <-.
+  assert (Csss : C s s s). apply imp_imp_context; exists x; split; auto.
+  pose proof (context_existence s t (ex_intro _ _ (conj Fxs Pstx))) as (u & Cust).
+  assert (exists v, C u s v /\ C v s t) as (v & Cusv & Cvst). context_asso s.
+  pose proof (context_unicity s t u v Cust Cvst) as <-.
+  pose proof (context_left_inject s t u u Cust Cusv) as <-.
   assumption.
 Qed.
 
+Lemma mutual_context_are_identity : forall s t u v,
+  C s t u -> C t s v -> s = t.
+Proof.
+  intros s t u v Cstu Ctsv.
+  assert (exists x, C s s x /\ C x v u) as (x & Cssx & Cxvu).
+  context_asso t.
+  assert (exists y, C t t y /\ C y u v) as (y & Cttx & Cyuv).
+  context_asso s.
+  pose proof (symmetric_context_are_slot_identity v u x y Cxvu Cyuv) as ->. 
+  pose proof (context_constraints u u y Cyuv) as (z & Fzu & Psuz).
+  assert (Cuuu: C u u u). apply imp_imp_context; exists z; split; auto.
+  unify_context Cuuu Cyuv.
+  unify_context Cxvu Cuuu.
+  unify_context Ctsv Cssx.
+  reflexivity.
+Qed.
+
 Definition SO s t := exists x, Ps s x /\ Ps t x.
 
-Theorem composition_same_owner : forall u s t,
-  C u s t -> exists x, Ps u x /\ Ps s x.
+Lemma SO_refl : forall s, S s -> SO s s.
+Proof.
+  intros s (x & Pssx).
+  exists x; split; auto.
+Qed.
+
+Lemma SO_symm : forall s t, SO s t -> SO t s.
+Proof.
+  intros s t (x & Pssx & Pstx).
+  exists x; split; auto.
+Qed.
+
+Lemma SO_trans : forall s t u, SO s t -> SO t u -> SO s u.
+Proof.
+  intros s t u (x & Pssx & Pstx) (y & Psty & Psuy).
+  unify_owner Pstx Psty.
+  exists x; split; auto.
+Qed.
+  
+Theorem context_same_owner : forall u s t,
+  C u s t -> SO u s.
 Proof.
   intros u s t Cust.
-  pose proof (compo_domains u s t Cust) as ([x Psux] & _).
+  pose proof (context_domains u s t Cust) as ([x Psux] & _).
   exists x.
   split; trivial.
   pose proof (whole_improper_slots x) as (v & Psvx & Fxv).
   exists u; assumption.
   pose proof (left_imp_composition v u x (conj Psvx Fxv) Psux) as Cuvu.
-  pose proof (compo_asso_rl u t v s u Cuvu Cust) as [z []].
-  pose proof (composition_constraints v s z H0) as [x0 [Fx0v Pssx0]].
-  pose proof (single_occupancy v x Psvx) as [v' [_ eq]].
-  apply eq in Fxv as ->, Fx0v as <-.
+  assert (exists z, C u z t /\ C z v s) as (z & _ & Czvs).
+  context_asso u.
+  pose proof (context_constraints v s z Czvs) as (x0 & Fx0v & Pssx0).
+  unify_filler Fxv Fx0v.
   assumption.
 Qed.
 
 (* Same Filler *)
-Theorem composition_same_filler : forall u s t,
-  C u s t -> exists x, F x u /\ F x t.
+Theorem context_same_filler : forall u s t,
+  C u s t -> exists a, F a u /\ F a t.
 Proof.
   intros u s t Cust.
-  pose proof (compo_domains u s t Cust) as ([x Psux] & _ & [z Pstz]).
+  pose proof (context_domains u s t Cust) as ([x Psux] & _ & [z Pstz]).
   pose proof (single_occupancy t z Pstz) as (a & Fat & _).
   clear z Pstz.
   exists a; split; trivial.
   pose proof (filler_has_imp_slot a t Fat) as (v & Psva & _).
-  pose proof (composition_existence t v a Fat Psva) as (u' & Cu'tv).
-  pose proof (composition_constraints s t u Cust) as (z & Fzs & Pstz).
-  pose proof (composition_same_owner u' t v Cu'tv) as (z' & Psu'z' & Pstz').
-  pose proof (single_owner t z Pstz) as PstUnique.
-  apply PstUnique in Pstz' as <-.
-  clear PstUnique.
+  pose proof (context_existence t v (ex_intro _ _ (conj Fat Psva))) as (u' & Cu'tv).
+  pose proof (context_constraints s t u Cust) as (z & Fzs & Pstz).
+  pose proof (context_same_owner u' t v Cu'tv) as (z' & Psu'z' & Pstz').
+  unify_owner Pstz Pstz'.
   rename Psu'z' into Psu'z.
-  pose proof (composition_existence s u' z Fzs Psu'z) as (w & Cwsu').
-  pose proof (compo_asso_rl w v s t u' Cwsu' Cu'tv) as (w' & Cww'v & Cw'st). 
-  pose proof (composition_unicity s t u w' Cust Cw'st) as <-.
-  rename Cww'v into Cwuv.
-  pose proof (composition_constraints u v w Cwuv) as (a' & Fa'u & Psva').
-  pose proof (single_owner v a Psva a' Psva') as <-.
+  pose proof (context_existence s u' (ex_intro _ _ (conj Fzs Psu'z))) as (w & Cwsu').
+  assert (exists w', C w w' v /\ C w' s t) as (w' & Cww'v & Cw'st).
+  context_asso u'. 
+  unify_context Cust Cw'st.
+  pose proof (context_constraints u v w Cww'v) as (a' & Fa'u & Psva').
+  unify_owner Psva Psva'.
   assumption.
 Qed.
 
-Theorem right_imp_composition_rev : forall s t,
-  C t t s -> exists x, IPs s x /\ F x t.
+(* BT7 *)
+Theorem parthood_transitivity_2 : forall a b c,
+  P a b -> P b c -> P a c.
+Proof.
+  intros a b c (s & Fas & Pssb) (t & Fbt & Pstc).
+  pose proof (context_existence t s (ex_intro _ _ (conj Fbt Pssb))) as (u & Cuts).
+  exists u.
+  pose proof (context_same_filler  _ _ _ Cuts) as (d & Fdu & Fds).
+  unify_filler Fas Fds.
+  pose proof (context_same_owner _ _ _ Cuts) as (d & Psud & Pstd).
+  unify_owner Pstc Pstd.
+  split; auto.
+Qed.
+
+Theorem right_imp_context_rev : forall s t,
+  C t t s -> exists a, IPs s a /\ F a t.
 Proof.
   intros s t Ctts.
-  pose proof (composition_constraints t s t Ctts) as (x & Fxt & Pssx).
+  pose proof (context_constraints t s t Ctts) as (x & Fxt & Pssx).
   exists x; repeat split; trivial.
-  pose proof (composition_same_filler t t s Ctts) as (y & Fyt & Fys).
-  pose proof (compo_domains t t s Ctts) as ((z & Pstz) & _).
-  pose proof (single_occupancy t z Pstz) as (a & Fat & FtUnique).
-  apply FtUnique in Fxt as ->, Fyt as <-.
+  pose proof (context_same_filler t t s Ctts) as (y & Fyt & Fys).
+  pose proof (context_domains t t s Ctts) as ((z & Pstz) & _).
+  unify_filler Fxt Fyt.
   assumption.
 Qed.
 
 Theorem imp_pro_compo_rev : forall s t,
-  C t s t -> exists x, IPs s x /\ Ps t x.
+  C t s t -> exists a, IPs s a /\ Ps t a.
 Proof.
   intros s t Ctst.
-  pose proof (composition_constraints s t t Ctst) as (x & Fxs & Pstx).
+  pose proof (context_constraints s t t Ctst) as (x & Fxs & Pstx).
   exists x; repeat split; trivial.
-  pose proof (composition_same_owner t s t Ctst) as (y & Psty & Pssy).
-  pose proof (single_owner t x Pstx y Psty) as <-.
+  pose proof (context_same_owner t s t Ctst) as (y & Psty & Pssy).
+  unify_owner Pstx Psty.
   assumption.
 Qed.
 
-Lemma mutual_compositions_are_identity : forall s t u v,
-  C s t u -> C t s v -> s = t.
+Theorem compo_stability : forall s t v s' t',
+  C s' v s -> C t' v t -> (forall u, C s t u <-> C s' t' u).
 Proof.
-  intros s t u v Cstu Ctsv.
-  pose proof (compo_asso_lr s t u s v Cstu Ctsv) as (x & Cssx & Cxvu).
-  pose proof (compo_asso_lr t s v t u Ctsv Cstu) as (y & Cttx & Cyuv).
-  pose proof (symmetric_compositions_are_slot_identity v u x y Cxvu Cyuv) as ->. 
-  pose proof (composition_unicity s t).
-  pose proof (composition_constraints u u y Cyuv) as (z & Fzu & Psuz).
-  pose proof (imp_imp_composition u z (conj Psuz Fzu)) as Cuuu.
-  pose proof (composition_unicity u u u y Cuuu Cyuv) as <-. 
-  apply composition_unicity with (s:=t) (t:=u); assumption.
+  intros s t v s' t' Cs'vs Ct'vt u.
+  split.
+  - intros Cstu.
+    assert (exists u', C u' t' u) as (u' & Cu't'u).
+    { pose proof (context_constraints _ _ _ Cstu) as (x & Fxt & Psux).
+      apply context_existence; exists x; split; auto.
+      pose proof (context_same_filler _ _ _ Ct'vt) as (y & Fyt' & Fyt).
+      unify_filler Fxt Fyt; auto.
+    }
+    enough (s' = u') as <-; auto.
+    assert (exists w, C u' v w /\ C w t u) as (w & Cu'vw & Cwtu).
+    context_asso t'.
+    unify_context Cstu Cwtu.
+    unify_context Cs'vs Cu'vw.
+    reflexivity.
+  - intros Cs't'u.
+    assert (exists w, C s' v w /\ C w t u) as (w & Cs'vw & Cwtu).
+    context_asso t'.
+    pose proof (context_left_inject _ _ _ _ Cs'vs Cs'vw) as <-.
+    auto.
 Qed.
 
 (****************
@@ -536,7 +580,7 @@ Definition PoS s t := exists u, C s t u.
 Lemma pos_domains : forall s t, PoS s t -> S s /\ S t.
 Proof.
   intros s t [u Cstu].
-  pose proof (compo_domains s t u Cstu) as (Ss & St & _).
+  pose proof (context_domains s t u Cstu) as (Ss & St & _).
   split; assumption.
 Qed.
 
@@ -545,7 +589,7 @@ Theorem conditional_pos_refl : forall s, S s -> PoS s s.
 Proof.
   intros s (x & Pssx).
   unfold PoS.  
-  pose proof (single_occupancy s x Pssx) as (z & Fzs & UniqueFzs).
+  pose proof (single_occupancy s x Pssx) as (z & Fzs & _).
   pose proof (general_conditional_refl z s) as [].
   right.
   assumption.
@@ -563,7 +607,7 @@ Theorem pos_antisym : forall s t,
   PoS s t -> PoS t s -> s = t.
 Proof.
   intros s t [u Cstu] [v Ctsv].
-  apply mutual_compositions_are_identity with (u:=u) (v:=v); assumption.
+  apply mutual_context_are_identity with (u:=u) (v:=v); assumption.
 Qed.
 
 (* PoS Transitivity *)
@@ -571,82 +615,62 @@ Theorem pos_trans : forall s t u,
   PoS s t -> PoS t u -> PoS s u.
 Proof.
   intros s t u [v Cstv] [w Ctuw]; move w before v.
-  pose proof (compo_asso_lr s t v u w Cstv Ctuw) as (x & Csux & _).
+  assert (exists x, C s u x /\ C x w v) as (x & Csux & _).
+  context_asso t.
   exists x; assumption.
 Qed.
 
 Theorem pos_same_owner : forall s t,
-  PoS s t -> exists x, Ps s x /\ Ps t x.
+  PoS s t -> SO s t.
 Proof.
   intros s t [u Cstu].
-  apply composition_same_owner with (u:=s) (s:=t) (t:=u).
+  apply context_same_owner with (u:=s) (s:=t) (t:=u).
   assumption.
 Qed.
 
-Lemma slots_are_parts_of_imp_slot : forall a s t,
-  IPs s a -> Ps t a -> PoS t s.
+Theorem ips_eq : forall a s, IPs s a -> (forall t, Ps t a <-> PoS t s).
 Proof.
-  intros a s t IPssa Psta.
-  exists t.
-  apply left_imp_composition with (x:=a); assumption.
-Qed.
-
-(* *)
-Theorem slots_constrain_fillers : forall a b s t,
-  F b t /\ F a s /\ PoS t s -> P b a.
-Proof.
-  intros a b s t [Fbt [Fas [u Ctsu]]].
-  pose proof (composition_constraints s u t Ctsu) as [a' [H H0]].
-  pose proof (composition_same_owner t s u Ctsu) as [z [Pstz Pssz]].
-  pose proof (single_occupancy s z Pssz) as [a'' [H1 H2]].
-  apply H2 in Fas as a''_eq_a, H as a''_eq_a'.
-  rewrite a''_eq_a in a''_eq_a'.
-  rewrite <- a''_eq_a' in H0.
-  clear a''_eq_a a''_eq_a' H1 H2 H a'' a'.
-  pose proof (composition_same_filler t s u Ctsu) as [x [H H1]].
-  pose proof (single_occupancy t z Pstz) as [x0 [H2 H3]].
-  apply H3 in Fbt as x0_eq_b, H as x0_eq_x.
-  rewrite x0_eq_x in x0_eq_b.
-  rewrite x0_eq_b in H1.
-  clear H2 H3 x0_eq_b x0_eq_x H.
-  unfold P.
-  exists u.
-  split; assumption.
+  intros a s.
+  intros IPssa t; split.
+  intros Psta; exists t; apply left_imp_composition with (a:=a); assumption.
+  intros PoSts; destruct IPssa as (Pssa & Fas).
+  pose proof (pos_same_owner _ _ PoSts) as (b & H & H1);
+  unify_owner Pssa H1; assumption.
 Qed.
 
-(* *)
-Theorem fillers_constrain_slots : forall a b s,
-  P b a -> IPs s a -> exists t, F b t /\ PoS t s.
+Theorem slots_constrain_fillers : forall a b,
+  (exists s t, F b t /\ F a s /\ PoS t s) <-> P b a.
 Proof.
-  intros a b s (t & Fbt & Psta) (PSsa & Fas).
-  exists t.
-  split; trivial.
-  exists t.
-  apply left_imp_composition with (x:=a); trivial.
-  split; trivial.
+  intros a b; split.
+  + intros (s & t & Fbt & Fas & [u Ctsu]).
+    pose proof (context_constraints s u t Ctsu) as (a' & Fa's & Psua).
+    unify_filler Fas Fa's.
+    pose proof (context_same_filler t s u Ctsu) as (b' & Fb't & Fb'u).
+    unify_filler Fbt Fb't.
+    exists u; split; auto.
+  + intros (t & Fbt & Psta).
+    pose proof (whole_improper_slots a) as (s & Pssa & Fas).
+    { exists t; auto. }
+    exists s, t; repeat split; auto.
+    exists t.
+    apply left_imp_composition with (a:=a); auto.
+    split; auto.
 Qed.
 
 (* PoS is stable under composition. *)
-Theorem pos_stability : forall s t u v w,
-  C v s t -> C w s u -> (PoS u t <-> PoS w v).
+Theorem pos_stability : forall s t u t' u',
+  C t' s t -> C u' s u -> (PoS u t <-> PoS u' t').
 Proof.
-  intros s t u v w Cvst Cwsu.
+  intros s t u t' u' Ct'st Cu'su.
+  pose proof (compo_stability _ _ _ _ _ Cu'su Ct'st).
   unfold PoS.
-  split.
-  (* Left-to-right *)
-  - intros (u' & Cutu').
-    exists u'.
-    pose proof (compo_asso_rl w u' s t u Cwsu Cutu') as (x & Cwxu' & Cxst).
-    pose proof (composition_unicity s t v x Cvst Cxst) as <-.
-    assumption.
-  (* Right-to-left *)
-  - intros (w' & Cwvw').
-    exists w'.
-    pose proof (compo_asso_lr w v w' s t Cwvw' Cvst) as (x & Cwsx & Cxtw).
-    pose proof (compo_left_inject s u x w Cwsu Cwsx) as <-.
-    assumption.
+  setoid_rewrite H.
+  reflexivity.
 Qed.
 
+(***************
+ * Proper Part *
+ ***************)
 Definition PPoS s t := PoS s t /\ s <> t.
 
 Theorem ppos_irrefl : forall s, ~ PPoS s s.
@@ -675,34 +699,85 @@ Proof.
     contradiction.
 Qed.
 
+Theorem ppos_same_owner: forall s t, PPoS s t -> SO s t.
+Proof.
+  intros s t [H _].
+  apply pos_same_owner; auto.
+Qed.
 
-Theorem proper_slots_are_parts_of_imp_slot :
-  forall s t x, IPs s x -> PPs t x -> PPoS t s.
+Theorem proper_slots_iff_parts_of_imp_slot :
+  forall s a, IPs s a -> (forall t, PPs t a <-> PPoS t s).
 Proof.
-  intros s t x IPssx [Pstx NFxt].
+  intros s a IPssa t.
+  pose proof (ips_eq a s IPssa).
+  unfold PPs, PPoS.
+  rewrite <- H.
+  destruct IPssa as (Pssa & Fas).
   split.
-  exists t.
-  apply left_imp_composition with (x:=x); assumption.
-  intros ->.
-  destruct IPssx.
-  contradiction.
+  + intros (Psta & nFat); split; auto.
+    intros ->; contradiction.
+  + intros (Psta & t_neq_s); split; auto.
+    intros Fat.
+    assert (IPssa: IPs s a) by (split; auto).
+    assert (IPsta: IPs t a) by (split; auto).
+    unify_improper_slot IPssa IPsta.
+    contradiction.
+Qed.
+
+Theorem slots_constrain_fillers_ppos : forall a b,
+  (exists s t, F b t /\ F a s /\ PPoS t s) <-> PP b a.
+Proof.
+  intros a b; split.
+  + intros (s & t & Fbt & Fas & (PoSts & t_neq_s)).
+    assert (Pba: P b a) by (apply slots_constrain_fillers; exists s, t; auto).
+    split; auto.
+    intros Pab.
+    pose proof (BT8 a b (conj Pab Pba)) as <-.
+    destruct PoSts as (u & Ctsu).
+    pose proof (context_constraints _ _ _ Ctsu) as (c & Fcs & Psua).
+    unify_filler Fas Fcs.
+    pose proof (context_same_filler _ _ _ Ctsu) as (c & Fct & Fau).
+    unify_filler Fbt Fct.
+    assert (IPsua: IPs u a) by (split; auto).
+    pose proof (right_imp_composition u s a IPsua Fas) as Cssu.
+    unify_context Ctsu Cssu.
+    contradiction.
+  + intros (Pba & nPab).
+    apply slots_constrain_fillers in Pba as (s & t & Fbt & Fas & PoSts).
+    exists s, t; repeat split; auto.
+    intros ->.
+    unify_filler Fas Fbt.
+    destruct nPab.
+    apply BT9.
+    pose proof (filler_has_imp_slot _ _ Fas) as (t & Psta & _).
+    exists t; auto.
 Qed.
 
 (* PPoS is stable under composition. *)
 Theorem ppos_stability : forall s t u v w,
-  PPoS u t -> C v s t -> C w s u -> PPoS w v.
+  C v s t -> C w s u -> (PPoS u t <-> PPoS w v).
 Proof.
-  intros s t u v w [(u' & Cutu') u_neq_t] Cvst Cwsu.
-  unfold PPoS.
+  intros s t u v w Cvst Cwsu.
   split.
-  exists u'.
-  pose proof (compo_asso_rl w u' s t u Cwsu Cutu') as (x & Cwxu' & Cxst).
-  pose proof (composition_unicity s t v x Cvst Cxst) as <-.
-  assumption.
-  intro h.
-  rewrite h in Cwsu.
-  pose proof (compo_left_inject s t u v Cvst Cwsu).
-  intuition.
+  - intros [(u' & Cutu') u_neq_t].
+    unfold PPoS.
+    split.
+    exists u'.
+    assert (exists x, C w x u' /\ C x s t) as (x & Cwxu' & Cxst).
+    context_asso u.
+    pose proof (context_unicity s t v x Cvst Cxst) as <-.
+    assumption.
+    intro h.
+    rewrite h in Cwsu.
+    pose proof (context_left_inject s t u v Cvst Cwsu).
+    intuition.
+  - intros [].
+    split.
+    pose proof (pos_stability s t u v w Cvst Cwsu) as ut_eq_wv.
+    + apply ut_eq_wv; assumption.
+    + intros ->.
+      apply H0.
+      apply context_unicity with (s:=s) (t:=t); assumption.
 Qed.
 
 (********************
@@ -712,12 +787,9 @@ Qed.
 Definition OoS s t := exists u, PoS u s /\ PoS u t.
 
 (* Conditional OoS Reflexivity *)
-Theorem cond_oos_refl : forall s,
-  S s -> OoS s s.
+Theorem cond_oos_refl : forall s, S s -> OoS s s.
 Proof.
-  intros s Ss.
-  unfold OoS.
-  exists s.
+  intros s Ss; exists s.
   pose proof (conditional_pos_refl s Ss).
   split; assumption.
 Qed.
@@ -734,24 +806,15 @@ Proof.
   assumption.
 Qed.
 
-Corollary oos_comm : forall s t,
-  OoS s t <-> OoS t s.
-Proof.
-  split; apply oos_symmetry.
-Qed.
-
 (* OoS Same Owner *)
 Theorem oos_same_owner : forall s t,
-  OoS s t -> (exists x, Ps s x /\ Ps t x).
+  OoS s t -> SO s t.
 Proof.
   intros s t [x [PoSxs PoSxt]].
   apply pos_same_owner in PoSxs as [sOwner []].
   apply pos_same_owner in PoSxt as [tOwner []].
-  pose proof (single_owner x sOwner H).
-  apply H3 in H1.
-  rewrite <- H1 in H2.
-  exists sOwner.
-  split; assumption.
+  unify_owner H H1.
+  exists sOwner; split; assumption.
 Qed.
 
 Lemma part_overlap_implies_whole_overlap: forall s t u,
@@ -763,18 +826,18 @@ Proof.
 Qed.
 
 Theorem slots_overlap_with_imp_slot :
-  forall s t x, IPs s x -> Ps t x -> OoS s t.
+  forall s t a, IPs s a -> Ps t a -> OoS s t.
 Proof.
   intros s t x IPssx Pstx.
   unfold OoS, PoS.
   exists t.
   split.
   - exists t.
-    apply left_imp_composition with (x:=x) ; assumption.
+    apply left_imp_composition with (a:=x) ; assumption.
   - pose proof (single_occupancy t x Pstx) as [y [Fyt _]].
     pose proof (filler_has_imp_slot y t Fyt) as [u IPsuy].
     exists u.
-    apply right_imp_composition with (x:=y); assumption.
+    apply right_imp_composition with (a:=y); assumption.
 Qed.
 
 Theorem pos_implies_overlap :
@@ -789,36 +852,43 @@ Qed.
 
 (* Overlap is stable under composition. *)
 (* OoS t u <-> OoS (s o t) (s o u) *)
-Lemma oos_stability : forall s t u v w,
-  C v s t -> C w s u -> (OoS t u <-> OoS v w).
+Lemma oos_stability : forall s t u t' u',
+  C t' s t -> C u' s u -> (OoS t u <-> OoS t' u').
 Proof.
-  intros s t u v w Cvst Cwsu.
+  intros s t u t' u' Ct'st Cu'su.
   split.
   (* Left-to-right *)
-  - intros (q & PoSqt & PoSqu).
+  - intros (v & PoSvt & PoSvu).
     unfold OoS.
-    pose proof (composition_constraints s t v Cvst) as (x & Fxs & Pstx).
-    pose proof (pos_same_owner q t PoSqt) as (y & Psqy & Psty).
-    pose proof (single_owner t x Pstx) as UniquePst.
-    apply UniquePst in Psty as <-.
-    rename Psqy into Psqx.
-    clear UniquePst.
-    pose proof (composition_existence s q x Fxs Psqx) as (q' & Cq'sq).
-    exists q'.
+    pose proof (context_constraints s t t' Ct'st) as (a & Fas & Psta).
+    pose proof (pos_same_owner v t PoSvt) as (b & Psva & Pstb).
+    unify_owner Psta Pstb.
+    pose proof (context_existence s v (ex_intro _ _ (conj Fas Psva))) as (v' & Cv'sv).
+    exists v'.
     split.
-    pose proof (pos_stability s t q v q' Cvst Cq'sq) as [Hstab _].
+    pose proof (pos_stability s t v t' v' Ct'st Cv'sv) as [Hstab _].
     apply Hstab; assumption.
-    pose proof (pos_stability s u q w q' Cwsu Cq'sq) as [Hstab _].
+    pose proof (pos_stability s u v u' v' Cu'su Cv'sv) as [Hstab _].
     apply Hstab; assumption.
-  - intros (x & PoSxv & PoSxw).
-    destruct PoSxv as (v' & Cxvv').
-    destruct PoSxw as (w' & Cxww').
-    pose proof (compo_asso_lr x v v' s t Cxvv' Cvst) as (x' & Cxsx' & Cx'tv').
-    pose proof (compo_asso_lr x w w' s u Cxww' Cwsu) as (x'' & Cxsx'' & Cx'uw').
-    pose proof (compo_left_inject s x' x'' x Cxsx' Cxsx'') as <-. 
-    clear Cxsx''.
-    exists x'.
-    split; [exists v'|exists w']; assumption.
+  - intros (v' & (vt & Cv't'vt) & (vu & Cv'u'vu)).
+    assert (exists v, C v' s v /\ C v t vt) as (v1 & Cv'sv1 & Cv1tvt).
+    context_asso t'.
+    assert (exists v, C v' s v /\ C v u vu) as (v2 & Cv'sv2 & Cv2uvu).
+    context_asso u'.
+    pose proof (context_left_inject _ _ _ _ Cv'sv1 Cv'sv2) as <-. 
+    clear Cv'sv2.
+    exists v1.
+    split; [exists vt|exists vu]; assumption.
+Qed.
+
+Theorem oos_constrains_o: forall a b s t,
+  OoS s t -> F a s -> F b t -> O a b.
+Proof.
+  intros a b s t (u & PoSus & PoSut) Fas Fbt.
+  pose proof (pos_domains _ _ PoSus) as ((d & Psud) & _).
+  pose proof (single_occupancy _ _ Psud) as (c & Fcu & _).
+  exists c; split; apply slots_constrain_fillers;
+  [ exists s, u | exists t, u]; auto.
 Qed.
 
 (*******************
@@ -826,70 +896,38 @@ Qed.
  *******************)
 
 Axiom slot_strong_supp : forall s t,
-  ~ PoS t s -> exists u, PoS u t /\ ~ OoS u s.
+  S s -> S t -> (~ PoS t s -> exists u, PoS u t /\ ~ OoS u s).
 
 Theorem slot_weak_supp : forall s t,
   PPoS s t -> exists u, PoS u t /\ ~ OoS u s.
 Proof.
   intros s t [].
-  apply slot_strong_supp.
+  pose proof (pos_domains _ _ H) as (Ss & St).
+  apply slot_strong_supp; auto.
   intro h.
   pose proof (pos_antisym s t H h).
   contradiction.
 Qed.
 
-Theorem slot_company : forall s t,
-  PPoS s t -> exists u, PPoS u t /\ u <> s.
-Proof.
-  intros s t [PoSst s_neq_t].
-  pose proof (slot_weak_supp s t (conj PoSst s_neq_t)) as (u & PoSut & NOus).
-  pose proof (pos_same_owner s t PoSst) as (x & H2 & _).
-  exists u.
-  repeat split; trivial;
-  intros ->; apply NOus.
-  apply oos_symmetry, pos_implies_overlap; assumption.
-  pose proof (conditional_pos_refl s) as [].
-  exists x; assumption.
-  exists s; split; trivial; exists x0; assumption.
-Qed.
-
-Theorem slot_strong_company : forall s t,
-  PPoS s t -> exists u, PPoS u t /\ ~PoS u s.
-Proof.
-  intros s t [PoSst s_neq_t].
-  pose proof (slot_weak_supp s t (conj PoSst s_neq_t)) as (u & PoSut & NOus).
-  exists u.
-  split.
-  - split; trivial.
-    intros ->.
-    apply NOus.
-    apply oos_symmetry, pos_implies_overlap.
-    assumption.
-  - intros PoSus.
-    apply NOus.
-    apply pos_implies_overlap.
-    assumption.
-Qed.
-
 Theorem oos_extensionality:
   forall s t, S s -> S t -> (forall u, OoS s u <-> OoS t u) -> s = t.
 Proof. 
-  intros s t _ _ s_eq_t.
+  intros s t Ss St s_eq_t.
   apply NNPP.
   intro s_ne_t.
   assert (~ PoS t s) as NPoSts.
   { intros PoSts.
     destruct (slot_weak_supp t s) as (u & PoSus & NOoSut). split; congruence.
     apply NOoSut.
-    rewrite oos_comm.
+    apply oos_symmetry.
     rewrite <- s_eq_t.
     exists u. split; trivial.
     pose proof (pos_same_owner u s PoSus) as (x & Psux & Pssx).
     apply conditional_pos_refl.
     exists x; assumption. }
-  pose proof (slot_strong_supp s t NPoSts) as (u & PoSut & NOoSus).
+  pose proof (slot_strong_supp _ _ Ss St NPoSts) as (u & PoSut & NOoSus).
   apply NOoSus.
-  rewrite oos_comm.
+  apply oos_symmetry.
   rewrite s_eq_t.
   exists u. split; trivial.
   pose proof (pos_same_owner u t PoSut) as (x & Psux & Pstx).
@@ -901,6 +939,7 @@ Theorem ppos_extensionality:
   forall s t, (exists u, PPoS u s \/ PPoS u t) -> (forall u, PPoS u s <-> PPoS u t) -> s = t.
 Proof.
   intros s t (u & H) s_eq_t.
+  assert (ppos_domains : forall s t, PPoS s t -> S s /\ S t) by (intros s' t' []; apply pos_domains; assumption).
   apply NNPP.
   intro s_ne_t.
   assert (~ PoS t s) as NPoSts.
@@ -909,7 +948,12 @@ Proof.
     split; congruence.
     apply s_eq_t in PPoSts as [_ t_neq_t].
     contradiction. }
-  pose proof (slot_strong_supp s t NPoSts) as (v & PoSvt & NOoSvs).
+  assert (Ss: S s) by (destruct H as [PPoSus|PPoSus]; [|apply s_eq_t in PPoSus];
+    pose proof (ppos_domains _ _ PPoSus) as [_ Ss]; assumption).
+  assert (St: S t)
+    by (destruct H as [PPoSut|PPoSut]; [apply s_eq_t in PPoSut|];
+    pose proof (ppos_domains _ _ PPoSut) as [_ St]; assumption).
+  pose proof (slot_strong_supp _ _ Ss St NPoSts) as (v & PoSvt & NOoSvs).
   assert (t = v) as <-.
   { apply NNPP.
     intros t_neq_v.
@@ -929,52 +973,34 @@ Qed.
 (****************
  * Sum of Slots *
  ****************)
- 
+
 Definition SoS u s t := PoS s u /\ PoS t u /\ forall v,
   (PoS v u -> (OoS s v \/ OoS t v)).
 
 Definition SoS2 u s t := forall v, (OoS u v <-> (OoS s v \/ OoS t v)).
 
-Theorem SoS_equal_SoS2 : forall u u' s t,
-  S u -> S u' -> SoS u s t -> SoS2 u' s t -> u = u'.
+Lemma sum_domains: forall s t u, SoS s t u -> S s /\ S t /\ S u.
 Proof.
-  intros u u' s t Su Su' (PoSsu & PoStu & H) H1.
-  unfold SoS2 in H1.
-  apply oos_extensionality; trivial.
-  intros w.
-  split.
-  - intros (x & PoSxu & PoSxw).
-    apply H in PoSxu.
-    apply H1 in PoSxu.
-    apply part_overlap_implies_whole_overlap with (t:=x); assumption.
-  - intros OoSu'w.
-    apply H1 in OoSu'w.
-    apply oos_comm.
-    destruct OoSu'w;
-    apply oos_comm in H0;
-    [apply part_overlap_implies_whole_overlap with (t:=s)|
-     apply part_overlap_implies_whole_overlap with (t:=t)];
-    assumption.
-Qed.
-
-Lemma SoS2_imp_Pos: forall s t u, SoS2 u s t -> PoS s u.
-Proof.
-  intros s t u H.
-  apply NNPP.
-  intros NPoSsu.
-  pose proof (slot_strong_supp u s NPoSsu) as (v & PoSvs & NOoSvu).
-  apply pos_implies_overlap in PoSvs.
-  destruct H with (v:=v).
-  destruct H1.
-  left; apply oos_comm; assumption.
-  apply NOoSvu.
-  exists x; apply and_comm; assumption.
+  intros s t u (PoSts & PoSus & _).
+  pose proof (pos_domains t s PoSts) as [].
+  pose proof (pos_domains u s PoSus) as [].
+  repeat split; assumption.
 Qed.
 
-Theorem SoS_equiv_SoS2: forall u s t,
-  (SoS u s t <-> SoS2 u s t).
+Theorem SoS_equiv_SoS2: forall s t, SO s t -> (forall u, SoS u s t <-> SoS2 u s t).
 Proof.
-  intros u s t.
+  assert (SoS2_imp_Pos: forall s t u, S s -> S u -> SoS2 u s t -> PoS s u).
+  {
+    intros s t u Ss Su H; apply NNPP; intros NPoSsu.
+    pose proof (slot_strong_supp _ _ Su Ss NPoSsu) as (v & PoSvs & NOoSvu).
+    apply pos_implies_overlap in PoSvs.
+    destruct H with (v:=v).
+    destruct H1.
+    left; apply oos_symmetry; assumption.
+    apply NOoSvu.
+    exists x; apply and_comm; assumption.
+  }
+  intros s t SOst u.
   split.
   - intros (PoSsu & PoStu & H) v.
     split.
@@ -984,92 +1010,71 @@ Proof.
       apply part_overlap_implies_whole_overlap with (t:=w);
       assumption.
     + intros [|];
-      apply oos_comm in H0;
-      apply oos_comm;
+      apply oos_symmetry in H0;
+      apply oos_symmetry;
       [apply part_overlap_implies_whole_overlap with (t:=s)|
        apply part_overlap_implies_whole_overlap with (t:=t)];
       assumption.
   - intros H.
+    assert (S s /\ S t /\ S u) as (Ss & St & Su).
+    { destruct SOst as (a & Pssa & Psta).
+      repeat split.
+      exists a; auto.
+      exists a; auto.
+      destruct H with (v:=s) as [_ H1].
+      destruct H1 as (v & PoSvu & PoSvs). left; apply cond_oos_refl; exists a; auto.
+      pose proof (pos_domains _ _ PoSvu) as (_ & Su); auto. }
     repeat split.
     + apply SoS2_imp_Pos with (t:=t); assumption.
-    + apply SoS2_imp_Pos with (t:=s).
+    + apply SoS2_imp_Pos with (t:=s); auto.
       unfold SoS2 in *.
       setoid_rewrite (or_comm (OoS s _)) in H.
       assumption.
     + intros v PoSvu.
       apply H.
-      apply oos_comm.
+      apply oos_symmetry.
       apply pos_implies_overlap.
       assumption.
 Qed.
 
-Theorem sum_domains: forall s t u, SoS s t u -> S s /\ S t /\ S u.
-Proof.
-  intros s t u (PoSts & PoSus & _).
-  pose proof (pos_domains t s PoSts) as [].
-  pose proof (pos_domains u s PoSus) as [].
-  repeat split; assumption.
-Qed.
-
-Theorem sum_implies_full_overlap: forall s t u,
-  SoS u s t -> (forall v, OoS v u <-> OoS s v \/ OoS t v).
-Proof.
-  intros s t u (PoSsu & PoStu & H_sum) w.
-  split.
-  - intros (x & PoSxw & PoSxu).
-    pose proof (H_sum x PoSxu).
-    destruct H as [OoSsx|OoStx];
-    [left|right];
-    apply part_overlap_implies_whole_overlap with (t:=x);
-    assumption.
-  - intros [|];
-    apply oos_symmetry in H;
-    [apply part_overlap_implies_whole_overlap with (t:=s)|apply part_overlap_implies_whole_overlap with (t:=t)];
-    assumption.
-Qed.
-
 (* Sum Existence *)
 Axiom sum_existence : forall s t x,
   Ps s x /\ Ps t x -> exists u, SoS u s t.
 
-(* Sum Unicity *)
-Theorem sum_unicity : forall s t u v,
-  (SoS u s t -> SoS v s t -> u = v).
-Proof.
-  intros s t u v SoSust SoSvst.
-  apply oos_extensionality.
-  destruct SoSust as [[] _].
-  apply compo_domains in H as (_ & H & _).
-  assumption.
-  destruct SoSvst as [[] _].
-  apply compo_domains in H as (_ & H & _).
-  assumption.
-  pose proof (sum_implies_full_overlap s t u SoSust).
-  pose proof (sum_implies_full_overlap s t v SoSvst).
-  intros w.
-  split.
-  - intros OoSuw.
-    apply oos_comm, H, H0, oos_comm in OoSuw.
-    assumption.
-  - intros OoSuw.
-    apply oos_comm, H0, H, oos_comm in OoSuw.
-    assumption. 
-Qed.
-
 (* Sum Same Owner *)
 Theorem sum_same_owner : forall s t u,
-  SoS u s t -> exists x, Ps u x /\ Ps s x /\ Ps t x.
+  SoS u s t -> exists a, Ps u a /\ Ps s a /\ Ps t a.
 Proof.
   intros s t u (PoSsu & PoStu & _).
   pose proof (pos_same_owner s u PoSsu) as [x []].
   pose proof (pos_same_owner t u PoStu) as [x0 []].
-  pose proof (single_owner u x H0).
-  apply H3 in H2.
-  rewrite <- H2 in H1.
+  unify_owner H0 H2.
   exists x.
   repeat split; assumption.
 Qed.
 
+(* Sum Unicity *)
+Theorem sum_unicity : forall s t u v,
+  (SoS u s t -> SoS v s t -> u = v).
+Proof.
+  intros s t u v SoSust SoSvst.
+  apply oos_extensionality.
+  - destruct SoSust as [H _].
+    apply pos_domains in H as (_ & H).
+    assumption.
+  - destruct SoSvst as [[] _].
+    apply context_domains in H as (_ & H & _).
+    assumption.
+  - pose proof (sum_domains _ _ _ SoSust) as (Su & Ss & St).
+    pose proof (sum_domains _ _ _ SoSvst) as (Sv & _).
+    pose proof (sum_same_owner _ _ _ SoSust) as (a & Psua & Pssa & Psta).
+    apply SoS_equiv_SoS2 in SoSust, SoSvst; auto.
+    intros w; split; intros OoSuw; 
+    [apply SoSvst, SoSust | apply SoSust, SoSvst];
+    assumption.
+    all: exists a; split; auto.
+Qed.
+
 (* Sum Idempotence *)
 Theorem sum_idempotence : forall s,
   S s -> SoS s s s.
@@ -1079,7 +1084,7 @@ Proof.
   repeat split; try (apply conditional_pos_refl; assumption).
   intros v PoSvs.
   apply pos_implies_overlap in PoSvs.
-  apply oos_comm in PoSvs.
+  apply oos_symmetry in PoSvs.
   left; assumption.
 Qed.
 
@@ -1093,54 +1098,27 @@ Proof.
   split; intros [H []]; repeat split; assumption.
 Qed.
 
-(* PoS t s -> s = s + t*)
-Theorem T1 : forall s t,
-  PoS t s -> SoS s s t.
+Lemma L47 : forall s t u, SO s t -> SoS u s t -> PoS s u.
 Proof.
-  intros s t PoSts.
-  pose proof (pos_same_owner t s PoSts) as [x []].
-  unfold SoS; repeat split.
-  apply conditional_pos_refl; exists x; assumption.
+  intros s t u SOst (PoSsu & _).
   assumption.
-  intros.
-  left.
-  unfold OoS.
-  exists v.
-  split; try assumption.
-  pose proof (pos_same_owner v s H1) as [x0 []].
-  apply conditional_pos_refl; exists x0; assumption.
-Qed.
-
-Theorem sum_imp_slot : forall s t x,
-  IPs s x -> Ps t x -> SoS s s t.
-Proof.
-  intros.
-  apply T1.
-  unfold PoS.
-  exists t.
-  apply left_imp_composition with (x:=x); assumption.
 Qed.
 
-Theorem T134 : forall s t u, SoS u s t -> PoS s u.
+Theorem L48 : forall s t u v, SO t u -> PoS s t -> SoS v t u -> PoS s v.
 Proof.
-  intros s t u (PoSsu & _).
-  assumption.
-Qed.
-
-Theorem T34 : forall s t u v, PoS s t -> SoS v t u -> PoS s v.
-Proof.
-  intros s t u v PoSst (PoStv & PoSuv & _).
+  intros s t u v _ PoSst (PoStv & PoSuv & _).
   apply pos_trans with (t:=t); assumption.
 Qed.
 
-Theorem T35 : forall s t u v,
-  SoS v s t -> PoS v u -> PoS s u.
+Lemma L49 : forall s t u v,
+  SO s t -> SoS v s t -> PoS v u -> PoS s u.
 Proof.
-  intros s t u v (PoSsv & _) PoSvu.
+  intros s t u v _ (PoSsv & _) PoSvu.
   apply pos_trans with (t:=v) ; assumption.
 Qed.
 
-Theorem T36 : forall s t, PoS s t <-> SoS t s t.
+(* PoS t s <-> s = s + t*)
+Theorem subpotence :  forall s t, PoS s t <-> SoS t s t.
 Proof.
   intros s t.
   split.
@@ -1151,14 +1129,156 @@ Proof.
     apply PoStt; exists x; assumption.
     intros v PoSvt.
     right.
-    apply oos_comm.
+    apply oos_symmetry.
     apply pos_implies_overlap.
     trivial.
   - intros (PoSst & _).
     trivial.
 Qed.
 
-(* OoS v s -> OoS v (s + t) *)
+Theorem overlap_sum_iff_operands: forall s t u,
+  (exists a, F a s /\ Ps t a /\ Ps u a) ->
+    forall tPu tPu' t' u', SoS tPu t u -> C tPu' s tPu -> C t' s t -> C u' s u ->
+      (forall v, OoS v tPu' <-> OoS v t' \/ OoS v u').
+Proof.
+  intros s t u (a & Fas & Psta & Psua) tPu tPu' t' u'
+    SoStPu C_tPu'_s_tPu Ct'st Cu'su v.
+  split.
+  - intros (w & PoSwv & [w1 C_w_tPu'_w1]).
+    assert (exists w2, C w s w2 /\ C w2 tPu w1) as (w2 & Cwsw2 & Cw2_tPu_w1)
+      by (context_asso tPu').
+    assert (PoS w2 tPu) as PoS_w2_tPu by (exists w1; auto).
+    destruct SoStPu as (PoSt_tPu & PoSu_tPu & H).
+    apply H in PoS_w2_tPu as [OoStw2|OoSuw2].
+    + pose proof (oos_stability _ _ _ _ _ Cwsw2 Ct'st) as oos_stab.
+      apply oos_symmetry in OoStw2.
+      apply oos_stab in OoStw2 as (w3 & PoSw3w & PoSw3t').
+      pose proof (pos_trans _ _ _ PoSw3w PoSwv) as PoSw3v.
+      left; exists w3; auto.
+    + pose proof (oos_stability _ _ _ _ _ Cwsw2 Cu'su) as oos_stab.
+      apply oos_symmetry in OoSuw2.
+      apply oos_stab in OoSuw2 as (w3 & PoSw3w & PoSw3u').
+      pose proof (pos_trans _ _ _ PoSw3w PoSwv) as PoSw3v.
+      right; exists w3; auto.
+  - intros [(w & PoSwv & PoSwt')|(w & PoSwv & PoSwu')].
+    + exists w; split; auto.
+      destruct PoSwt' as (w' & Cwt'w').
+      assert (exists w2, C w s w2 /\ C w2 t w') as (w2 & Cwsw2 & Cw2tw')
+        by (context_asso t').
+      destruct SoStPu as (PoSt & _).
+      destruct PoSt as (t2 & Ct_tPu_t2).
+      assert (exists w3, C w2 tPu w3 /\ C w3 t2 w') as (w3 & Cw2_tPu_w3 & Cw3t2w')
+        by (context_asso t).
+      pose proof (context_asso s tPu w3 w) as [(x & Cwxw3 & CxstPu) _].
+      exists w2; split; auto.
+      unify_context C_tPu'_s_tPu CxstPu.
+      exists w3; auto.
+    + exists w; split; auto.
+      destruct PoSwu' as (w' & Cwu'w').
+      assert (exists w2, C w s w2 /\ C w2 u w') as (w2 & Cwsw2 & Cw2uw')
+        by (context_asso u').
+      destruct SoStPu as (_ & PoSu & _).
+      destruct PoSu as (u2 & Cu_tPu_u2).
+      assert (exists w3, C w2 tPu w3 /\ C w3 u2 w') as (w3 & Cw2_tPu_w3 & Cw3u2w')
+        by (context_asso u).
+      pose proof (context_asso s tPu w3 w) as [(x & Cwxw3 & CxstPu) _].
+      exists w2; split; auto.
+      unify_context C_tPu'_s_tPu CxstPu.
+      exists w3; auto.
+Qed.
+
+Theorem left_distributivity: forall s t u tPu tPu'1 t' u' tPu'2,
+  (exists a, F a s /\ Ps t a /\ Ps u a) ->
+    SoS tPu t u -> C tPu'1 s tPu -> C t' s t -> C u' s u -> SoS tPu'2 t' u' ->
+      tPu'1 = tPu'2.
+Proof.
+  intros s t u tPu tPu'1 t' u' tPu'2 H SoStu C_tPu'1 Ct'st Cu'su SoStPu'2.
+  apply oos_extensionality.
+  - pose proof (context_domains _ _ _ C_tPu'1) as (StPu'1 & _); auto.
+  - pose proof (sum_domains _ _ _ SoStPu'2) as (StPu'2 & _); auto.
+  - pose proof (overlap_sum_iff_operands s t u H
+        tPu tPu'1 t' u' SoStu C_tPu'1 Ct'st Cu'su).
+    apply SoS_equiv_SoS2 in SoStPu'2.
+    unfold SoS2 in SoStPu'2.
+    intros w.
+    rewrite SoStPu'2.
+    assert (oos_comm: forall s t, OoS s t <-> OoS t s)
+      by (intros s0 t0; split; apply oos_symmetry).
+    setoid_rewrite (oos_comm).
+    apply H0.
+    pose proof (sum_same_owner _ _ _ SoStPu'2) as (a & _ & Pst'a & Psu'a).
+    exists a; auto.
+Qed.
+
+Lemma L53 : forall a s t u, F a s -> SoS u s t -> F a u -> s = u.
+Proof.
+  intros a s t u Fas ((s' & Csus') & PoStu & H) Fau.
+  pose proof (context_same_filler _ _ _ Csus') as (a' & Fa's & Fas').
+  unify_filler Fas Fa's.
+  pose proof (context_constraints _ _ _ Csus') as (a' & Fa'u &  Pss'a).
+  unify_filler Fau Fa'u.
+  pose proof (right_imp_composition _ _ _ (conj Pss'a Fas') Fau) as Cuus'.
+  unify_context Csus' Cuus'.
+  reflexivity.
+Qed.
+
+Theorem right_distrib: forall s t u v w x y,
+  SoS v s t -> C w v u -> C x s u -> C y t u -> s = t.
+Proof.
+  intros s t u v w x y ((s' & Csvs') & (t' & Ctvt') & _) Cwvu Cxsu Cytu.
+  pose proof (context_constraints _ _ _ Cwvu) as (a & Fav & Psua).
+
+  assert (s = v).
+  { pose proof (context_same_filler _ _ _ Csvs') as (e & Fes & Fes').
+    pose proof (context_constraints _ _ _ Cxsu) as (b & Fbs & Psub).
+    unify_owner Psua Psub.
+    unify_filler Fbs Fes.
+    pose proof (context_constraints _ _ _ Csvs') as (f & Ffv & Pss'f).
+    unify_filler Fav Ffv.
+    pose proof (right_imp_composition s' v a (conj Pss'f Fes') Fav) as Cvvs'.
+    pose proof (context_unicity _ _ _ _ Csvs' Cvvs') as s_eq_v.
+    assumption. }
+  
+  assert (t = v).
+  { pose proof (context_same_filler _ _ _ Ctvt') as (i & Fit & Fit').
+    pose proof (context_constraints _ _ _ Cytu) as (c & Fcy & Psuc).
+    unify_owner Psua Psuc.
+    unify_filler Fcy Fit.
+    pose proof (context_constraints _ _ _ Ctvt') as (g & Fgv & Pst'g).
+    unify_filler Fav Fgv.
+    pose proof (right_imp_composition _ _ _ (conj Pst'g Fit') Fav) as Cvvt'.
+    pose proof (context_unicity _ _ _ _ Ctvt' Cvvt') as t_eq_v.
+    assumption. }
+  rewrite H, H0.
+  reflexivity.
+Qed.
+
+Lemma left_distrib_ref: forall a b c s t u,
+  C a s t -> C b s u -> SoS c a b -> (exists d, SoS d t u /\ C c s d).
+Proof.
+  intros a b c s t u Cast Cbsu SoScab.
+  pose proof (context_constraints s t a Cast) as (x & Fxs & Pstx).
+  pose proof (context_constraints s u b Cbsu) as (y & Fys & Psuy).
+  unify_filler Fxs Fys.
+  rename Psuy into Psux.
+  pose proof (sum_existence t u x (conj Pstx Psux)) as (d & SoSdtu).
+  exists d.
+  split; trivial.
+  pose proof (sum_same_owner t u d SoSdtu) as (y & Psdx & Psty & _).
+  unify_owner Pstx Psty.
+  pose proof (context_existence s d (ex_intro _ _ (conj Fxs Psdx))) as (e & Cesd).
+  pose proof (left_distributivity s t u d e a b c (ex_intro _ _ (conj Fxs (conj Pstx Psux)) ) SoSdtu Cesd Cast Cbsu SoScab) as <-.
+  assumption.
+Qed.
+
+Lemma pos_sum : forall s t u v,
+  PoS s v -> PoS t v -> SoS u s t -> PoS u v.
+Proof.
+  intros s t u v [s' Csvs'] [t' Ctvt'] SoSust.
+  pose proof (left_distrib_ref s t u v s' t' Csvs' Ctvt' SoSust) as (w & SoSws't' & Cuvw).
+  exists w; assumption.
+Qed.
+
 Lemma L1 : forall s t u v,
   SoS u s t -> OoS v s -> OoS v u.
 Proof.
@@ -1171,21 +1291,6 @@ Proof.
   apply pos_trans with (t:=s) ; assumption.
 Qed.
 
-(* OoS v (s o t) -> OoS v (s o (t + u)) *)
-Lemma L2 : forall s t u v a b c,
-  C a s t -> SoS b t u -> C c s b -> OoS v a -> OoS v c.
-Proof.
-  intros s t u v a b c Cast ([t' Ctbt'] & _) Ccsb [x [PoSxv [x1 Cxax1]]].
-  exists x.
-  split; trivial.
-  pose proof (compo_asso_lr x a x1 s t Cxax1 Cast) as [x2 [Cxsx2 Cx2tx1]].
-  pose proof (compo_asso_lr x2 t x1 b t' Cx2tx1 Ctbt') as [x3 [Cx2bx3 _]].
-  exists x3.
-  pose proof (compo_asso_rl x x3 s b x2 Cxsx2 Cx2bx3) as [x4 [Cxx4x3 Cx4sb]].
-  pose proof (composition_unicity s b c x4 Ccsb Cx4sb) as <-.
-  assumption.
-Qed.
-
 (* OoS v (s + t) -> OoS s v \/ OoS t v *)
 Lemma L3 : forall s t u v,
   SoS u s t -> OoS v u -> OoS s v \/ OoS t v.
@@ -1197,87 +1302,6 @@ Proof.
   assumption.
 Qed.
 
-(* OoS v (s o (t + u)) -> OoS (v, s o t) \/ OoS(v, s o u) *)
-Lemma L4 : forall s t u v a b c d,
-  SoS a t u -> C b s a -> OoS v b -> C c s t -> C d s u -> OoS v c \/ OoS v d.
-Proof.
-  intros s t u v a b c d ([t' Ctat'] & [u' Cuau'] & H_sum) Cbsa (r & [w Crvw] & [q' Crbq']) Ccst Cdsu.
-  pose proof (compo_asso_lr r b q' s a Crbq' Cbsa) as (q & Crsq & Cqaq').
-  assert (PoSqa : PoS q a) by (exists q'; assumption).
-  pose proof (H_sum q PoSqa) as [OoStq|OoSuq].
-  - left.
-    apply oos_stability with (s:=s) (v:=c) (w:=r) in OoStq as (x & PoSxc & PoSxr); trivial.
-    exists x.
-    split; trivial.
-    apply pos_trans with (t:=r); trivial.
-    exists w; assumption.
-  - right.
-    apply oos_stability with (s:=s) (v:=d) (w:=r) in OoSuq as (x & PoSxc & PoSxr); trivial.
-    exists x.
-    split; trivial.
-    apply pos_trans with (t:=r); trivial.
-    exists w; assumption.
-Qed.
-
-(* OoS v (s o t + s o u) <-> OoS v (s o (t + u)) *)
-Lemma L5 : forall s t u a b c d e,
-  C b s t -> C c s u -> SoS a b c -> SoS d t u -> C e s d -> (forall v, OoS v a <-> OoS v e).
-Proof.
-  intros s t u a b c d e Cbst Ccsu SoSabc SoSdtu Cesd v.
-  split.
-  (* Left to right *)
-  - intro OoSva.
-    pose proof (L3 b c a v SoSabc OoSva) as [OoSbv|OoScv].
-    + apply oos_symmetry in OoSbv as OoSvb.
-      pose proof (L2 s t u v b d e Cbst SoSdtu Cesd OoSvb).
-      assumption.
-    + apply oos_symmetry in OoScv as OoSvc.
-      apply sum_commutativity in SoSdtu as SoSdut.
-      pose proof (L2 s u t v c d e Ccsu SoSdut Cesd OoSvc).
-      assumption.
-  (* Right to left *)
-  - intro OoSve.
-    pose proof (L4 s t u v d e b c SoSdtu Cesd OoSve Cbst Ccsu) as [OoSvb|OoSvc].
-    + pose proof (L1 b c a v SoSabc OoSvb).
-      assumption.
-    + apply sum_commutativity in SoSabc as SoSacb.
-      pose proof (L1 c b a v SoSacb OoSvc).
-      assumption.
-Qed.
-
-Theorem left_distributivity: forall s t u a b c d e,
-  SoS a t u -> C b s a -> C c s t -> C d s u -> SoS e c d -> b = e.
-Proof.
-Admitted.
-
-Theorem left_distrib_ref: forall a b c s t u,
-  C a s t -> C b s u -> SoS c a b -> (exists d, SoS d t u /\ C c s d).
-Proof.
-  intros a b c s t u Cast Cbsu SoScab.
-  pose proof (composition_constraints s t a Cast) as (x & Fxs & Pstx).
-  pose proof (composition_constraints s u b Cbsu) as (y & Fys & Psuy).
-  pose proof (single_filler s x Fxs y Fys) as <-.
-  rename Psuy into Psux.
-  clear Fys.
-  pose proof (sum_existence t u x (conj Pstx Psux)) as (d & SoSdtu).
-  exists d.
-  split; trivial.
-  pose proof (sum_same_owner t u d SoSdtu) as (y & Psdx & Psty & _).
-  pose proof (single_owner t x Pstx y Psty) as <-.
-  clear Psty.
-  pose proof (composition_existence s d x Fxs Psdx) as (e & Cesd).
-  pose proof (left_distributivity s t u d e a b c SoSdtu Cesd Cast Cbsu SoScab) as <-.
-  assumption.
-Qed.
-
-Lemma pos_sum : forall s t u v,
-  PoS s v -> PoS t v -> SoS u s t -> PoS u v.
-Proof.
-  intros s t u v [s' Csvs'] [t' Ctvt'] SoSust.
-  pose proof (left_distrib_ref s t u v s' t' Csvs' Ctvt' SoSust) as (w & SoSws't' & Cuvw).
-  exists w; assumption.
-Qed.
-
 (* Sum Associativity *)
 Theorem sum_associativity : forall s t u a b c d,
   SoS a s t -> SoS b a u -> SoS d s c -> SoS c t u -> b = d.
@@ -1297,75 +1321,174 @@ Proof.
     destruct SoSdsc as (PoSsd & PoScd & H).
     apply H in PoSvd as [OoSsv|OoScv].
     + left.
-      apply oos_comm.
+      apply oos_symmetry.
       apply L1 with (s:=s) (t:=t); trivial.
-      apply oos_comm; assumption.
-    + apply oos_comm in OoScv.
+      apply oos_symmetry; assumption.
+    + apply oos_symmetry in OoScv.
       pose proof (L3 t u c v SoSctu OoScv) as [OoStv|OoSuv].
       * left.
-        apply oos_comm.
+        apply oos_symmetry.
         apply L1 with (s:=t) (t:=s).
         apply sum_commutativity; assumption.
-        apply oos_comm; assumption.
+        apply oos_symmetry; assumption.
       * right; assumption.
 Qed.
 
-Theorem sum_asso2: forall s t u a b c d,
-  SoS a s t -> SoS b a u -> SoS d s c -> SoS c t u -> b = d.
+Theorem sum_stability: forall u s t v, Cb u v -> Cb s v -> Cb t v -> 
+  (forall u' s' t', C u' v u /\ C s' v s /\ C t' v t -> SoS u s t <-> SoS u' s' t').
+Proof.
+  intros u s t v (a & Fav & Psua) (b & Fbv & Pssa) (c & Fcv & Psta) u' s' t' (Cu'vu & Cs'vs & Ct'vt).
+  unify_filler Fav Fbv.
+  unify_filler Fav Fcv.
+  pose proof (pos_stability _ _ _ _ _ Cu'vu Cs'vs) as PoSsu_stab.
+  pose proof (pos_stability _ _ _ _ _ Cu'vu Ct'vt) as PoStu_stab.
+  unfold SoS; rewrite PoSsu_stab, PoStu_stab; repeat apply and_iff_compat_l.
+  split; intros H.
+  - intros w' [x Cwu'x].
+    assert (exists w, C w' v w /\ C w u x) as (w & Cw'vw & Cwux) by (context_asso u') .
+    pose proof (oos_stability _ _ _ _ _ Cs'vs Cw'vw) as H1.
+    pose proof (oos_stability _ _ _ _ _ Ct'vt Cw'vw) as H2.
+    rewrite <- H1, <- H2.
+    apply H; exists x; auto.
+  - intros w PoSwu.
+    pose proof (pos_same_owner _ _ PoSwu) as (b & Pswb & Psub).
+    unify_owner Psua Psub.
+    assert (exists w', C w' v w) as [w' Cw'vw].
+    apply context_existence; exists a; split; auto.
+    pose proof (oos_stability v _ _ _ _ Cs'vs Cw'vw) as H2.
+    rewrite H2.
+    pose proof (oos_stability v _ _ _ _ Ct'vt Cw'vw) as H3.
+    rewrite H3.
+    apply H.
+    pose proof (pos_stability v _ _ _ _ Cu'vu Cw'vw) as H1.
+    rewrite <- H1.
+    auto.
+Qed.
+
+(**********
+ * Fusion *
+ **********)
+Definition FoS z (phi: Entity -> Prop) :=
+  (forall w, phi w -> PoS w z) /\ (forall v, PoS v z -> (exists w, phi w /\ OoS v w)).
+
+Axiom FoS_existence:
+  forall phi, (exists w, phi w /\ (forall v, phi v -> SO w v))
+    -> (exists z, FoS z phi).
+
+Theorem FoS_unicity: 
+  forall (phi : Entity -> Prop) s t, (exists w, phi w) 
+    -> FoS s phi -> FoS t phi -> s = t.
+Proof.
+  intros phi s t [w phiW] [H1 H2] [H3 H4].
+  apply oos_extensionality.
+  { apply H1, pos_domains in phiW as [_ Ss].
+    assumption. }
+  { apply H3, pos_domains in phiW as [_ St].
+    assumption. }
+  intros u; split.
+  - intros (a & PoSas & PoSau).
+    pose proof (H2 a PoSas) as (b & phiB & (c & PoSca & PoScb)).
+    pose proof (H3 b phiB) as PoSbt.
+    pose proof (pos_trans c a u PoSca PoSau) as PoScu.
+    pose proof (pos_trans c b t PoScb PoSbt) as PoSct.
+    exists c; split; assumption.
+  - intros (a & PoSat & PoSau).
+    pose proof (H4 a PoSat) as (b & phiB & (c & PoSca & PoScb)).
+    pose proof (H1 b phiB) as PoSbs.
+    pose proof (pos_trans c a u PoSca PoSau) as PoScu.
+    pose proof (pos_trans c b s PoScb PoSbs) as PoScs.
+    exists c; split; assumption.
+Qed.
+
+Ltac unify_fusion FoS1 Fos2 :=
+  pose proof (FoS_unicity _ _ _ FoS1 Fos2);
+  subst; clear Fos2.
+
+Theorem conditioned_FoS_iff_SoS: forall s t u, FoS u (fun w => w = s \/ w = t) <-> SoS u s t.
+Proof.
+  intros s t u.
+  split.
+  + intros [H H0].
+    repeat split; try apply H; auto.
+    intros v PoSvu.
+    pose proof (H0 v PoSvu) as (w & H1).
+    destruct H1.
+    apply oos_symmetry in H2.
+    destruct H1 as [-> | ->]; auto.
+  + intros (PoSsu & PoStu & H).
+    split.
+    intros w [-> | ->]; auto.
+    intros v PoSvu.
+    pose proof (H v PoSvu) as []; apply oos_symmetry in H0; [exists s | exists t ]; split; auto.
+Qed.
 
+Theorem slot_is_fusion_of_its_slots: forall s, FoS s (fun w => PoS w s).
+Proof.
+  intros s.
+  split; auto.
+  intros v PoSvs.
+  exists v; split; auto.
+  apply cond_oos_refl.
+  pose proof (pos_same_owner _ _ PoSvs) as (a & Psva & _).
+  exists a; auto.
+Qed.
 
-Lemma sss_contra : forall s t,
-   (forall u, ~ PoS u t \/ OoS u s) -> PoS t s.
+Theorem ips_is_fusion: forall a s, Ps s a -> (exists t, IPs t a /\ FoS t (fun w => Ps w a)).
 Proof.
-  intros s t H.
-  apply NNPP.
-  intros NPoSts.
-  pose proof (slot_strong_supp s t NPoSts) as (u & PoSut & NOoSus).
-  pose proof (H u).
-  destruct H0; contradiction.
-Qed.
-
-Theorem test_1 : forall a s t u tPu,
-  IPs s a -> PPs t a -> PPs u a -> SoS tPu t u ->
-    (forall v, PPs v a -> v = t \/ v = u) -> s = tPu.
-Proof.
-  intros a s t u tPu [Pssa Fas] [Psta NFat] [Psua NFau] SoStPu v_eq_t_or_u.
-  pose proof (sum_same_owner t u tPu SoStPu) as (a' & PspTua' & Psta' & _).
-  pose proof (single_owner t a Psta a' Psta') as <-.
-  clear Psta'.
-  rename PspTua' into PspTua.
-  pose proof (sum_domains tPu t u SoStPu) as (StPu & St & Su).
-  apply pos_antisym.
-  (* Proof of PoS s (t + u) *)
-  * apply sss_contra.
-    intros v.
-    apply imply_to_or.
-    intros PoSvs.
-    destruct (classic (v = s)) as [v_eq_s|v_neq_s].
-    - rewrite v_eq_s.
-      exists tPu.
-      split.
-      + exists tPu.
-        apply left_imp_composition with (x:=a).
-        split. all: assumption.
-      + apply conditional_pos_refl; assumption.
-    - assert (PPs v a) as PPsva.
-      (* Proof of PPs v a *)
-      { pose proof (pos_same_owner v s PoSvs) as (a' & Psva' & Pssa').
-        pose proof (single_owner s a Pssa a' Pssa') as <-.
-        clear Pssa'.
-        rename Psva' into Psva.
-        split. assumption.
-        intros Fav.
-        pose proof (unique_improper_slot a s v (conj Pssa Fas) (conj Psva Fav)) as <-.
-        contradiction. }
-      pose proof (v_eq_t_or_u v PPsva).
-      destruct SoStPu as (PoSttPu & PoSutPu & H2).
-      destruct H as [->| ->];
-      [exists t|exists u]; split; trivial;
-      apply conditional_pos_refl;
-      exists a; assumption.
-  (* Proof of PoS (t+u) s *)
-  * apply slots_are_parts_of_imp_slot with (a:=a).
-    split. all: assumption.
+  intros a s Pssa.
+  pose proof (whole_improper_slots a) as (t & IPsta).
+  exists s; assumption.
+  exists t; split; auto.
+  pose proof (ips_eq a t IPsta).
+  unfold FoS.
+  setoid_rewrite H.
+  apply slot_is_fusion_of_its_slots.
+Qed.
+
+Theorem fusion_stability : forall (phi : Entity -> Prop) s s' t,
+  C s' t s -> (forall w, phi w -> exists w', C w' t w ) -> (FoS s phi <-> FoS s' (fun w' => exists w, C w' t w /\ phi w)).
+Proof.
+  intros phi s s' t Cs'ts H.
+  split.
+  - intros [H1 H2].
+    split.
+    + intros w (w' & Cwtw' & phi_w').
+      pose proof (H1 _ phi_w') as PoSw's.
+      pose proof (pos_stability _ _ _ _ _ Cs'ts Cwtw') as pos_stab.
+      rewrite pos_stab in PoSw's; auto.
+    + intros v (v' & Cvs'v').
+      assert (exists v'', C v t v'' /\ C v'' s v') as (v'' & Cvtv'' & Cv''sv).
+      context_asso s'.
+      pose proof (H2 v'') as (w'' & phiw'' & OoSv''w'').
+      exists v'; auto.
+      pose proof (H1 w'' phiw'') as PoSw''s.
+      pose proof (pos_same_owner w'' s PoSw''s) as (a & Psw''a & Pssa).
+      pose proof (context_constraints _ _ _ Cs'ts) as (b & Fat & Pssb).
+      unify_owner Pssa Pssb.
+      pose proof (context_existence t w'' (ex_intro _ _ (conj Fat Psw''a))) as (w''' & Cw'''tw'').
+      exists w'''; split.
+      exists w''; auto.
+      pose proof (oos_stability t v'' w'' v w''' Cvtv'' Cw'''tw'') as oos_stab.
+      apply oos_stab; auto.
+  - intros [H1 H2].
+    split.
+    + intros w phiW.
+      pose proof (H w phiW) as (w' & Cw'tw).
+      pose proof (pos_stability t s w s' w' Cs'ts Cw'tw) as pos_stab.
+      apply pos_stab, H1.
+      exists w; split; auto.
+    + intros v' (v & Cv'sv).
+      assert (exists v'', C v'' s' v) as (v'' & Cv''s'v).
+      { pose proof (context_constraints _ _ _ Cv'sv) as (a & Fas & Psua).
+        pose proof (context_same_filler _ _ _ Cs'ts) as (b & Fas' & Fbs).
+        unify_filler Fas Fbs.
+        apply context_existence; exists a; split; auto. }
+      pose proof (H2 v'') as (w & (w' & Cwtw' & phiw') & OoSv''w).
+      exists v; auto.
+      exists w'; split; auto.
+      assert (exists u, C v'' t u /\ C u s v) as (u & Cv''tu & Cusv).
+      context_asso s'.
+      unify_context Cv'sv Cusv.
+      pose proof (oos_stability _ _ _ _ _ Cv''tu Cwtw') as oos_stab.
+      apply oos_stab; auto.
 Qed.