diff --git a/slot_mereology.v b/slot_mereology.v
new file mode 100644
index 0000000000000000000000000000000000000000..b8994681825586d82dfe057f125535f7186ac255
--- /dev/null
+++ b/slot_mereology.v
@@ -0,0 +1,1371 @@
+Require Import Setoid.
+Require Import Classical.
+
+(***********
+ *         *
+ * Bennett *
+ *         *
+ ***********)
+Parameter Entity: Set.
+Parameter F : Entity -> Entity -> Prop.
+Parameter Ps : Entity -> Entity -> Prop.
+Definition P x y := exists s, F x s /\ Ps s y.
+Definition PP x y := P x y /\ ~ P y x.
+Definition O x y := exists z, P z x /\ P z y.
+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.
+
+(* Slots Cannot Fill *)
+Axiom slots_cannot_fill : forall x y,
+  F x y -> ~exists z, Ps x z.
+
+(* Slots Don’t Have Slots *)
+Axiom slots_dont_have_slots : forall x y,
+  Ps x y -> ~exists z, Ps z x.
+
+(* Filler Irreflexivity *)
+Theorem BT1 : forall x,
+  ~ F x x.
+Proof.
+  intros x h.
+  apply only_slots_are_filled in h as h1.
+  apply slots_cannot_fill in h as h2.
+  contradiction.
+Qed.
+
+(* Filler Asymmetry *)
+Theorem BT2 : forall x y,
+  F x y -> ~ F y x.
+Proof.
+  intros x y H.
+  apply only_slots_are_filled in H.
+  intro h.
+  apply slots_cannot_fill in h.
+  contradiction.
+Qed.
+
+(* Filler Transitivity *)
+Theorem BT3 : forall x y z,
+  (F x y /\ F y z) -> F x z.
+Proof.
+  intros x y z [].
+  apply only_slots_are_filled in H as [].
+  apply slots_cannot_fill in H0 as [].
+  exists x0.
+  apply H.
+Qed.
+
+(* Slot Irreflexivity *)
+Theorem BT4 : forall x,
+  ~Ps x x.
+Proof.
+  intros x h.
+  apply slots_dont_have_slots in h as h1.
+  destruct h1.
+  exists x.
+  assumption.
+Qed.
+
+(* Slot Asymmetry *)
+Theorem BT5 : forall x y,
+  Ps x y -> ~ Ps y x.
+Proof.
+  intros x y H h.
+  apply slots_dont_have_slots in h as [].
+  exists x.
+  assumption.
+Qed.
+
+(* Slot Transitivity *)
+Theorem BT6 : forall x y z,
+  (Ps x y /\ Ps y z) -> Ps x z.
+Proof.
+  intros x y z [].
+  apply slots_dont_have_slots in H0 as [].
+  exists x.
+  assumption.
+Qed.
+
+(* Improper Parthood Slots *)
+Axiom whole_improper_slots : forall x,
+  (exists y, Ps y x) -> (exists z, Ps z x /\ F x z).
+
+(* Slot Inheritance *)
+Axiom slot_inheritance : forall x y z1 z2,
+  (Ps z1 y /\ F x z1) /\ Ps z2 x -> Ps z2 y.
+
+(* Mutual Occupancy is Identity *)
+Axiom mutual_occupancy : forall x y z1 z2,
+  (Ps z1 y /\ F x z1) /\ (Ps z2 x /\ F y z2) -> x = y.
+
+(* Single Occupancy *)
+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.
+
+(* Parthood Transitivity *)
+Theorem parthood_transitivity : forall x y z,
+  (P x y /\ P y z) -> P x z.
+Proof.
+  firstorder.
+  unfold P.
+  eauto 6 using slot_inheritance.
+Qed.
+
+(* Anti-Symmetry *)
+Theorem BT8 : forall x y,
+  (P x y /\ P y x) -> x = y.
+Proof.
+  unfold P.
+  firstorder.
+  apply mutual_occupancy with (z1 := x1) (z2 := x0).
+  auto.
+Qed.
+
+(* Conditional Reflexivity *)
+Theorem BT9 : forall x,
+  (exists z, Ps z x) -> P x x.
+Proof.
+  intros x h.
+  apply whole_improper_slots in h as [y ].
+  unfold P.
+  exists y.
+  apply and_comm; assumption.
+Qed.
+
+(* Parts <-> Slots *)
+Theorem BT11 : forall y,
+  ((exists x, P x y) <-> (exists z, Ps z y)).
+Proof.
+  intro y.
+  unfold P.
+  split.
+  - intros [x [s []]].
+    exists s.
+    assumption.
+  - intros [z Pszy].
+    apply single_occupancy in Pszy as H1.
+    destruct H1 as [x []].
+    exists x, z.
+    split; assumption.
+Qed.
+
+(* Composites <-> Slot-Composites *)
+Theorem BT12 : forall y,
+  ((exists x, PP x y) <-> (exists z, PPs z y)).
+Proof.
+  unfold PP, PPs, P.
+  intro b.
+  split.
+  (* left to right *)
+  - intros [a [[c [Fac Pscb]] nPba]].
+    exists c.
+    split.
+    -- apply Pscb.
+    -- pose proof (single_occupancy _ _ Pscb) as [d [Fdc Uc]].
+       intros Fbc.
+       pose proof (Uc a Fac). subst.
+       pose proof (Uc b Fbc). subst.
+       apply nPba.
+       exists c; split.
+       apply Fbc.
+       apply Pscb.
+  (* right to left *)
+  - intros [a [Psab nFba]].
+    pose proof (single_occupancy _ _ Psab) as [c [Fca Uc]].
+    exists c.
+    split.
+    + exists a; split; eauto.
+    + intros [d [Fbd Psfc]].
+    apply nFba.
+    assert (b = c) as Heqbc.
+    * eapply mutual_occupancy with (z1 := d) (z2 := a).
+      repeat split; assumption.
+    * rewrite Heqbc in *.
+      apply Fca.
+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)).
+
+(* Slot Weak Supplementation *)
+Theorem BT13 : forall x y,
+  (PP x y -> (exists z, Ps z y /\ ~ Ps z x)).
+Proof.
+  intros a b [[c [Fac Pscb]] nPba].
+  pose proof (whole_improper_slots b).
+  destruct H.
+  exists c.
+  exact Pscb.
+  exists x.
+  split.
+  apply H.
+  intro h.
+  apply nPba.
+  destruct H.
+  exists x.
+  split; assumption.
+Qed.
+
+(* Slot Extensionality *)
+(* This is not a theorem of the theory. *)
+Theorem BT14 : forall x y,
+  ((exists z, PP z x) \/ (exists z, PP z y)) ->
+    ((x = y) <->
+      (exists z, PPs z x <-> PPs z y)).
+Abort.
+
+(**********************
+ *                    *
+ * Tarbouriech et al. *
+ *                    *
+ **********************)
+
+Definition S s := exists x, Ps s x.
+
+(* Single Owner *)
+Axiom single_owner : forall s x,
+  Ps s x -> forall y, Ps s y -> x = y.
+
+(* Anti-Inheritance *)
+Theorem anti_inheritance : forall x y s t,
+  x <> y /\ Ps s y /\ F x s /\ Ps t x -> ~Ps t y.
+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.
+Qed.
+
+Definition IPs x y := Ps x y /\ F y x.
+
+(* 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.
+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.
+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.
+Proof.
+  intros x s [Pssx _].
+  apply single_owner.
+  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.
+
+(* General Conditional Reflexivity *)
+Lemma general_conditional_refl : forall x s,
+  Ps s x \/ F x s -> P x x.
+Proof.
+  intros x s Ps_or_F.
+  apply BT9.
+  destruct Ps_or_F as [Pssx|Fxs].
+  - exists s; assumption.
+  - pose proof (filler_has_imp_slot x s Fxs) as (t & Pstx & _).
+    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.
+
+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.
+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.
+Qed.
+
+(***************
+ * Composition *
+ ***************)
+
+Parameter C : Entity -> Entity -> Entity -> Prop.
+
+Axiom compo_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.
+
+Axiom composition_constraints : forall s t u,
+  C u s t -> exists x, F x s /\ Ps t x.
+
+(* Composition Unicity *)
+Axiom composition_unicity : forall s t u v,
+  C u s t -> C v s t -> u = v.
+
+Axiom compo_left_inject : forall s t u v,
+  C v s t -> C v s u -> t = u.
+
+Axiom compo_right_inject : forall s t u v x,
+  C v t s -> C v u s -> IPs s x -> t = u.
+
+Theorem symmetric_compositions_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.
+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 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.
+
+(* 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.
+
+(* Improper-Improper Composition *)
+(* 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.
+Qed.
+
+(* Proper-Improper Composition *)
+Theorem right_imp_composition : forall s t x,
+  IPs s x -> F x 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 <-.
+  assumption.
+Qed.
+
+(* Improper-Proper Composition *)
+Theorem left_imp_composition : forall s t x,
+  IPs s x -> Ps t x -> 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 <-.
+  assumption.
+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.
+Proof.
+  intros u s t Cust.
+  pose proof (compo_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 <-.
+  assumption.
+Qed.
+
+(* Same Filler *)
+Theorem composition_same_filler : forall u s t,
+  C u s t -> exists x, F x u /\ F x t.
+Proof.
+  intros u s t Cust.
+  pose proof (compo_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.
+  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 <-.
+  assumption.
+Qed.
+
+Theorem right_imp_composition_rev : forall s t,
+  C t t s -> exists x, IPs s x /\ F x t.
+Proof.
+  intros s t Ctts.
+  pose proof (composition_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 <-.
+  assumption.
+Qed.
+
+Theorem imp_pro_compo_rev : forall s t,
+  C t s t -> exists x, IPs s x /\ Ps t x.
+Proof.
+  intros s t Ctst.
+  pose proof (composition_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 <-.
+  assumption.
+Qed.
+
+Lemma mutual_compositions_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.
+  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.
+Qed.
+
+(****************
+ * Part of Slot *
+ ****************)
+
+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 & _).
+  split; assumption.
+Qed.
+
+(* Conditional PoS Reflexivity *)
+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 (general_conditional_refl z s) as [].
+  right.
+  assumption.
+  exists x0.
+  pose proof (right_imp_composition x0 s z).
+  unfold IPs in H0.
+  apply H0.
+  destruct H.
+  repeat split.
+  all: assumption.
+Qed.
+
+(* PoS Anti-Symmetry *)
+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.
+Qed.
+
+(* PoS Transitivity *)
+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 & _).
+  exists x; assumption.
+Qed.
+
+Theorem pos_same_owner : forall s t,
+  PoS s t -> exists x, Ps s x /\ Ps t x.
+Proof.
+  intros s t [u Cstu].
+  apply composition_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.
+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.
+Qed.
+
+(* *)
+Theorem fillers_constrain_slots : forall a b s,
+  P b a -> IPs s a -> exists t, F b t /\ PoS t s.
+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.
+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).
+Proof.
+  intros s t u v w Cvst Cwsu.
+  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.
+Qed.
+
+Definition PPoS s t := PoS s t /\ s <> t.
+
+Theorem ppos_irrefl : forall s, ~ PPoS s s.
+Proof.
+  intros s [_ ].
+  contradiction.
+Qed.
+
+Theorem ppos_asym : forall s t,
+  PPoS s t -> ~ PPoS t s.
+Proof.
+  intros s t [] [].
+  pose proof (pos_antisym s t H H1).
+  contradiction.
+Qed.
+
+Theorem ppos_trans : forall s t u,
+  PPoS s t -> PPoS t u -> PPoS s u.
+Proof.
+  intros s t u [] [].
+  split.
+  - apply pos_trans with (t:=t) ; assumption.
+  - intro h.
+    rewrite <- h in H1.
+    pose proof (pos_antisym s t H H1).
+    contradiction.
+Qed.
+
+
+Theorem proper_slots_are_parts_of_imp_slot :
+  forall s t x, IPs s x -> PPs t x -> PPoS t s.
+Proof.
+  intros s t x IPssx [Pstx NFxt].
+  split.
+  exists t.
+  apply left_imp_composition with (x:=x); assumption.
+  intros ->.
+  destruct IPssx.
+  contradiction.
+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.
+Proof.
+  intros s t u v w [(u' & Cutu') u_neq_t] Cvst Cwsu.
+  unfold PPoS.
+  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.
+Qed.
+
+(********************
+ * Overlap of Slots *
+ ********************)
+
+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.
+Proof.
+  intros s Ss.
+  unfold OoS.
+  exists s.
+  pose proof (conditional_pos_refl s Ss).
+  split; assumption.
+Qed.
+
+(* OoS Symmetry *)
+Theorem oos_symmetry : forall s t,
+  OoS s t -> OoS t s.
+Proof.
+  unfold OoS.
+  intros.
+  destruct H as [x H].
+  exists x.
+  apply and_comm.
+  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).
+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.
+Qed.
+
+Lemma part_overlap_implies_whole_overlap: forall s t u,
+  OoS u t -> PoS t s -> OoS u s.
+Proof.
+  intros s t u [v [PoSvu PoSvt]] PoSts.
+  exists v; split; trivial.
+  apply pos_trans with (t:=t); assumption.
+Qed.
+
+Theorem slots_overlap_with_imp_slot :
+  forall s t x, IPs s x -> Ps t x -> 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.
+  - 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.
+Qed.
+
+Theorem pos_implies_overlap :
+  forall s t, PoS s t -> OoS s t.
+Proof.
+  intros s t PoSst.
+  exists s; split; trivial.
+  pose proof (pos_same_owner s t PoSst) as (x & Pssx & _).
+  apply conditional_pos_refl.
+  exists x; assumption.
+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).
+Proof.
+  intros s t u v w Cvst Cwsu.
+  split.
+  (* Left-to-right *)
+  - intros (q & PoSqt & PoSqu).
+    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'.
+    split.
+    pose proof (pos_stability s t q v q' Cvst Cq'sq) as [Hstab _].
+    apply Hstab; assumption.
+    pose proof (pos_stability s u q w q' Cwsu Cq'sq) 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.
+Qed.
+
+(*******************
+ * Supplementation *
+ *******************)
+
+Axiom slot_strong_supp : forall 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.
+  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.
+  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.
+    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).
+  apply NOoSus.
+  rewrite oos_comm.
+  rewrite s_eq_t.
+  exists u. split; trivial.
+  pose proof (pos_same_owner u t PoSut) as (x & Psux & Pstx).
+  apply conditional_pos_refl.
+  exists x; assumption.
+Qed.
+
+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.
+  apply NNPP.
+  intro s_ne_t.
+  assert (~ PoS t s) as NPoSts.
+  { intros PoSts.
+    assert (PPoS t s) as PPoSts.
+    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 (t = v) as <-.
+  { apply NNPP.
+    intros t_neq_v.
+    assert (PPoS v t) as PPoSvt.
+    split; congruence.
+    apply s_eq_t in PPoSvt as [PoSvs _].
+    apply pos_implies_overlap in PoSvs.
+    contradiction. }
+  apply NOoSvs.
+  exists u.
+  destruct H as [H1|H1];
+  apply s_eq_t in H1 as H2;
+  destruct H1, H2;
+  split; assumption.
+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'.
+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.
+Qed.
+
+Theorem SoS_equiv_SoS2: forall u s t,
+  (SoS u s t <-> SoS2 u s t).
+Proof.
+  intros u s t.
+  split.
+  - intros (PoSsu & PoStu & H) v.
+    split.
+    + intros (w & PoSwu & PoSwv).
+      pose proof (H w PoSwu) as [H1|H1];
+      [left|right];
+      apply part_overlap_implies_whole_overlap with (t:=w);
+      assumption.
+    + intros [|];
+      apply oos_comm in H0;
+      apply oos_comm;
+      [apply part_overlap_implies_whole_overlap with (t:=s)|
+       apply part_overlap_implies_whole_overlap with (t:=t)];
+      assumption.
+  - intros H.
+    repeat split.
+    + apply SoS2_imp_Pos with (t:=t); assumption.
+    + apply SoS2_imp_Pos with (t:=s).
+      unfold SoS2 in *.
+      setoid_rewrite (or_comm (OoS s _)) in H.
+      assumption.
+    + intros v PoSvu.
+      apply H.
+      apply oos_comm.
+      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.
+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.
+  exists x.
+  repeat split; assumption.
+Qed.
+
+(* Sum Idempotence *)
+Theorem sum_idempotence : forall s,
+  S s -> SoS s s s.
+Proof.
+  intros s Ss.
+  unfold SoS.
+  repeat split; try (apply conditional_pos_refl; assumption).
+  intros v PoSvs.
+  apply pos_implies_overlap in PoSvs.
+  apply oos_comm in PoSvs.
+  left; assumption.
+Qed.
+
+(* Sum Commutativity *)
+Theorem sum_commutativity : forall s t u,
+  (SoS u s t <-> SoS u t s).
+Proof.
+  intros s t u.
+  unfold SoS.
+  setoid_rewrite (or_comm (OoS s _)).
+  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.
+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.
+  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.
+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 & _).
+  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.
+Proof.
+  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.
+Proof.
+  intros s t.
+  split.
+  - intros PoSst.
+    pose proof (pos_same_owner s t PoSst) as (x & _ & Pstx).
+    pose proof (conditional_pos_refl t) as PoStt.
+    unfold SoS; repeat split; trivial.
+    apply PoStt; exists x; assumption.
+    intros v PoSvt.
+    right.
+    apply oos_comm.
+    apply pos_implies_overlap.
+    trivial.
+  - intros (PoSst & _).
+    trivial.
+Qed.
+
+(* OoS v s -> OoS v (s + t) *)
+Lemma L1 : forall s t u v,
+  SoS u s t -> OoS v s -> OoS v u.
+Proof.
+  intros s t u v SoSust [x []].
+  unfold OoS.
+  exists x.
+  split.
+  assumption.
+  destruct SoSust as [PoSsu [PoStu _]].
+  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.
+Proof.
+  intros s t u v [PoSsu [PoStu H_sum]] [x [PoSxv PoSxu]].
+  pose proof (H_sum x PoSxu) as [OoSsx|OoStx];
+  [left|right];
+  apply part_overlap_implies_whole_overlap with (t:=x);
+  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.
+Proof.
+  intros s t u a b c d  SoSast SoSbau SoSdsc SoSctu.
+  enough (SoS d a u).
+  apply sum_unicity with (s:=a) (t:=u); assumption.
+  repeat split.
+  - apply pos_sum with (s:=s) (t:=t).
+    destruct SoSdsc; assumption.
+    destruct SoSdsc as (_ & PoScd & _), SoSctu as (PoStc & _).
+    apply pos_trans with (t:=c); assumption.
+    assumption.
+  - destruct SoSdsc as (_ & PoScd & _), SoSctu as (_ & PoScu & _).
+    apply pos_trans with (t:= c); assumption.
+  - intros v PoSvd.
+    destruct SoSdsc as (PoSsd & PoScd & H).
+    apply H in PoSvd as [OoSsv|OoScv].
+    + left.
+      apply oos_comm.
+      apply L1 with (s:=s) (t:=t); trivial.
+      apply oos_comm; assumption.
+    + apply oos_comm in OoScv.
+      pose proof (L3 t u c v SoSctu OoScv) as [OoStv|OoSuv].
+      * left.
+        apply oos_comm.
+        apply L1 with (s:=t) (t:=s).
+        apply sum_commutativity; assumption.
+        apply oos_comm; 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.
+
+
+Lemma sss_contra : forall s t,
+   (forall u, ~ PoS u t \/ OoS u s) -> PoS t s.
+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.
+Qed.