diff --git a/CDS_prims.v b/CDS_prims.v
new file mode 100755
index 0000000..9692313
--- /dev/null
+++ b/CDS_prims.v
@@ -0,0 +1,87 @@
+(* CDS_prims- (hopefully) the final version *)
+Axiom e prop world                  : Set.
+Axiom w0                            : world.
+Axiom tv                            : prop -> world -> bool.
+Axiom truth falsity                 : prop.
+Axiom p_not                         : prop -> prop.
+Axiom p_and p_or p_implies p_iff    : prop -> prop -> prop.
+
+Section Statterm.
+    Inductive statterm : Set := ent : statterm | prp : statterm | func : statterm -> statterm -> statterm.
+
+    (* Mapping statterms to the appropriate sense type *)
+    Fixpoint Sns (s : statterm) : Set
+        :=  match s with
+                | ent       => e
+                | prp       => prop
+                | func a b  => (Sns a) -> (Sns b)
+            end.
+
+    (* Mapping statterms to the appropriate extensional type *)
+    Fixpoint Ext (s : statterm) : Set
+        :=  match s with
+                | ent       => e
+                | prp       => bool
+                | func a b  => (Sns a) -> (Ext b)
+            end.
+
+    (* Definition of the "@" function *)
+    Fixpoint ext_at (s : statterm) : (Sns s) -> world -> (Ext s)
+        :=  match s as t return ((Sns t) -> world -> (Ext t)) with
+                | ent       => fun (x : e) (w : world) => x
+                | prp       => tv
+                | func a b  => fun (f : (Sns a) -> (Sns b)) (w : world) (x : Sns a) => ext_at b (f x) w
+            end.
+End Statterm.
+
+Axiom p_equals                      : forall s : statterm, (Sns s) -> (Sns s) -> prop.
+Axiom p_exists p_forall             : forall s : statterm, ((Sns s) -> prop) -> prop.
+
+Module Sem_notations.
+    (* Adding a new "sem_scope" for these notations- should allow us to use "not" w/o naming conflicts *)
+    Infix "and"         := p_and            (at level 80)   : sem_scope.
+    Infix "or"          := p_or             (at level 80)   : sem_scope.
+    Infix "implies"     := p_implies        (at level 80)   : sem_scope.
+    Infix "iff"         := p_iff            (at level 80)   : sem_scope.
+    Infix "equals"      := (p_equals prp)   (at level 80)   : sem_scope.
+    Notation "'not' p"  := (p_not p)        (at level 80)   : sem_scope.
+    Notation "p @ w"    := (tv p w)         (at level 80)   : sem_scope. (* hopefully this'll make the theorems way more legible! *)
+    Open Scope sem_scope.
+    (* we'll see if I make another bool_prims file, in which case these 3 lines'll go in there *)
+    Infix    "~>"       := implb            (at level 50)   : bool_scope.
+    Notation "-~ x"     := (negb x)         (at level 50)   : bool_scope.
+    Open Scope bool_scope.
+End Sem_notations.
+Import Sem_notations.
+
+(*  Ok, so this last part uses Coq's module system to define the ultrafilter here but defining entails in extensions.v
+    Feel free to ignore the details of how this works (this stuff's annoyed me since the days I was messing around with OCaml),
+    but here's a brief explanation:
+    Basically, I'm defining a type of "file" (aka a module) and what such a file must contain to be well-typed (this is Ent).
+    In this case, all I require of modules of the type Ent is that they provide a term p_entails of type prop -> prop -> Prop.
+    Then, I define Ult which is a "functor" (their word) on files/modules of this type, meaning that it takes modules which are
+    of type Ent and returns another module (modules aren't required to have types, since they're language-external notions).
+    From there, I can make all of my definitions in terms of the p_entails provided by the argument module. *)
+Module Type Ent.
+    Parameter p_entails : prop -> prop -> Prop.
+End Ent.
+
+Module Ult (E : Ent).
+    Definition p_equiv : prop -> prop -> Prop := fun p q : prop => (E.p_entails p q) /\ (E.p_entails q p).
+    Infix "entails"     := E.p_entails  (at level 80)   : sem_scope.
+    Infix "≡"           := p_equiv      (at level 80)   : sem_scope.
+
+    Definition pset : Set := prop -> bool.
+    Definition facts: world -> pset := fun (w : world) (p : prop) => tv p w.
+
+    Definition uc  : pset -> Prop := fun s : pset => forall p q : prop,  (s p) = true  -> p entails q -> (s q) = true.
+    Definition ac  : pset -> Prop := fun s : pset => forall p q : prop,  (s p) = true  -> (s q) = true -> (s (p and q)) = true.
+    Definition sai : pset -> Prop := fun s : pset => forall p   : prop, ((s p) = true) \/ ((s (not p)) = true).
+    Definition cst : pset -> Prop := fun s : pset => (s falsity) = false.
+    Definition ultrafilter : pset -> Prop := fun s : pset => (uc s) /\ (ac s) /\ (sai s) /\ (cst s).
+
+    Axiom facts_inj  : forall w v : world, (facts w) = (facts v) -> w = v.
+    Axiom facts_onto : forall s : pset, (ultrafilter s) -> exists w : world, s = (facts w).
+End Ult.
+
+
diff --git a/extensions.v b/extensions.v
new file mode 100755
index 0000000..017862f
--- /dev/null
+++ b/extensions.v
@@ -0,0 +1,310 @@
+(* extensions- (hopefully) the final version of worlds_prim/entails_def *)
+
+Load CDS_prims.
+
+Module entails_def.
+    Definition p_entails := fun p q : prop => forall w : world, (p@w) = true -> (q@w) = true.
+End entails_def.
+
+Module Import Ultra := Ult entails_def.
+
+Section prop_axioms.
+    Axiom p_and_ax      : forall (p q : prop) (w : world), ((p and q)@w) = ((p@w) && (q@w)).
+    Axiom p_or_ax       : forall (p q : prop) (w : world), ((p or q)@w) = ((p@w) || (q@w)).
+    Axiom p_implies_ax  : forall (p q : prop) (w : world), ((p implies q)@w) = ((p@w) ~> (q@w)).
+    Axiom p_iff_ax      : forall (p q : prop) (w : world), ((p iff q)@w) = (((p implies q)@w) && ((q implies p)@w)).
+    Axiom p_not_ax      : forall (p   : prop) (w : world), ((not p)@w) = -~(p@w).
+    Axiom truth_ax      : forall w : world, (truth@w)   = true.
+    Axiom falsity_ax    : forall w : world, (falsity@w) = false.
+    Axiom p_equals_ax   : forall (s : statterm) (x y : (Sns s)) (w : world), (((p_equals s x y)@w) = true) <-> (x = y).
+    Axiom p_exists_ax   : forall (s : statterm) (R : (Sns s) -> prop) (w : world),
+        (((p_exists s R)@w) = true) <-> ~(forall x : (Sns s), ((R x)@w) = false).
+    Axiom p_forall_ax   : forall (s : statterm) (R : (Sns s) -> prop) (w : world),
+        (((p_forall s R)@w) = true) <-> (forall x : (Sns s), ((R x)@w) = true).
+End prop_axioms.
+
+Section Useful_lemmas.
+    Definition eq_trans' : forall {A : Type} {x y z : A}, x = y -> x = z -> y = z
+        := fun (A : Type) (x y z : A) (u : x = y) (v : x = z) => match u in (_ = a) return (a = z) with eq_refl => v end.
+
+    Definition tnf : true <> false := eq_ind true (fun b : bool => if b then True else False) I false.
+End Useful_lemmas.
+
+Section prop_Theorems.
+    Definition facts_ultra  : forall w : world, ultrafilter (facts w)
+        :=   fun w : world =>
+             conj   (fun (p q : prop) (e : (p@w) = true) (f : p entails q) => f w e)
+            (conj   (fun (p q : prop) (u : (p@w) = true) (v : (q@w) = true) => eq_trans (p_and_ax p q w) (f_equal2 andb u v))
+            (conj   (fun p : prop => (if (p@w) as b return ((p@w) = b -> ((p@w) = true) \/ (((not p)@w) = true))
+                                      then (fun u : (p@w) = true => or_introl u)
+                                      else (fun v : (p@w) = false => or_intror (eq_trans (p_not_ax p w) (f_equal negb v))))
+                                    eq_refl)
+                    (falsity_ax w))).
+
+    Definition entail_refl  : forall p : prop, p entails p
+        := fun (p : prop) (w : world) (e : (p@w) = true) => e.
+
+    Definition entail_trans : forall p q r : prop, (p entails q) -> (q entails r) -> (p entails r)
+        := fun (p q r : prop) (f : p entails q) (g : q entails r) (w : world) (e : (p@w) = true) => g w (f w e).
+
+    Definition p_and_e1     : forall p q : prop, (p and q) entails p
+        :=  fun (p q : prop) (w : world) (e : ((p and q)@w) = true) =>
+            (if (p@w) as b return ((b && (q@w)) = true -> b = true)
+             then (fun u : (q@w) = true => eq_refl)
+             else (fun v : false = true => v))
+            (eq_trans' (p_and_ax p q w) e).
+
+    Definition p_and_e2     : forall p q : prop, (p and q) entails q
+        :=  fun (p q : prop) (w : world) (e : ((p and q)@w) = true) =>
+            (if (p@w) as b return ((b && (q@w)) = true -> (q@w) = true)
+             then (fun u : (q@w) = true => u)
+             else (fun v : false = true => if (q@w) as c return (c = true) then eq_refl else v))
+            (eq_trans' (p_and_ax p q w) e).
+
+    Definition p_and_i      : forall p q r : prop, p entails q -> p entails r -> p entails (q and r)
+        :=  fun (p q r : prop) (f : p entails q) (g : p entails r) (w : world) (e : (p@w) = true) =>
+            eq_trans (p_and_ax q r w) (f_equal2 andb (f w e) (g w e)).
+
+    Definition p_or_e       : forall p q r : prop, p entails r -> q entails r -> (p or q) entails r
+        :=  fun (p q r : prop) (f : p entails r) (g : q entails r) (w : world) (e : ((p or q)@w) = true) =>
+            (if (p@w) as b return ((p@w) = b -> (b || (q@w)) = true -> (r@w) = true)
+              then (fun (u : (p@w) = true) (v : true = true) => f w u)
+              else (fun x : (p@w) = false => g w))
+            eq_refl
+            (eq_trans' (p_or_ax p q w) e).
+
+    Definition p_or_i1      : forall p q : prop, p entails (p or q)
+        := fun (p q : prop) (w : world) (e : (p@w) = true) => eq_trans (p_or_ax p q w) (f_equal (fun b : bool => b || (q@w)) e).
+
+    Definition p_or_i2      : forall p q : prop, q entails (p or q)
+        :=  fun (p q : prop) (w : world) (e : (q@w) = true) =>
+            eq_trans (p_or_ax p q w) (if (p@w) as b return ((b || (q@w)) = true) then eq_refl else e).
+
+    Definition truth_top    : forall p : prop, p entails truth
+        := fun (p : prop) (w : world) (e : (p@w) = true) => truth_ax w.
+
+    Definition falsity_bot  : forall p : prop, falsity entails p
+        :=  fun (p : prop) (w : world) (e : (falsity@w) = true) =>
+            if (p@w) as b return (b = true) then eq_refl else (eq_trans' (falsity_ax w) e).
+
+    Definition p_implies_i  : forall p q r : prop, (p and q) entails r -> p entails (q implies r)
+        :=  fun (p q r : prop) (f : (p and q) entails r) (w : world) (e : (p@w) = true) =>
+            eq_trans    (p_implies_ax q r w)
+                        ((if (q@w) as c return ((q@w) = c -> (c ~> (r@w)) = true)
+                         then (fun u : (q@w) = true => f w (eq_trans (p_and_ax p q w) (f_equal2 andb e u)))
+                         else (fun v : (q@w) = false => eq_refl))
+                         eq_refl).
+
+    Definition p_implies_e  : forall p q : prop, (p and (p implies q)) entails q
+        :=  fun (p q : prop) (w : world) (e : ((p and (p implies q))@w) = true) =>
+            eq_trans'   (eq_trans (p_implies_ax p q w) (f_equal (fun b : bool => b ~> (q@w)) (p_and_e1 p (p implies q) w e)))
+                        (p_and_e2 p (p implies q) w e).
+
+    Definition complement : forall (p : prop) (w : world), ((p and (not p))@w) = false
+        :=  fun (p : prop) (w : world) =>
+            eq_trans    (eq_trans (p_and_ax p (not p) w) (f_equal (andb (p@w)) (p_not_ax p w)))
+                        (if (p@w) as b return ((b && -~b) = false) then eq_refl else eq_refl).
+
+    Definition lem : forall (p : prop) (w : world), ((p or (not p))@w) = true
+        :=  fun (p : prop) (w : world) =>
+            eq_trans    (eq_trans (p_or_ax p (not p) w) (f_equal (orb (p@w)) (p_not_ax p w)))
+                        (if (p@w) as b return ((b || -~b) = true) then eq_refl else eq_refl).
+
+    Definition dne : forall p : prop, (not (not p)) entails p
+        :=  fun (p : prop) (w : world) (e : ((not (not p))@w) = true) =>
+            (if (p@w) as b return (-~(-~b) = true -> b = true) then (fun u : true = true => u) else (fun v : false = true => v))
+            (eq_trans' (eq_trans (p_not_ax (not p) w) (f_equal negb (p_not_ax p w))) e).
+
+    Definition p_forall_e : forall (s : statterm) (R : (Sns s) -> prop) (x : (Sns s)), (p_forall s R) entails (R x)
+        :=  fun (s : statterm) (R : (Sns s) -> prop) (x : (Sns s)) (w : world) (e : ((p_forall s R)@w) = true) =>
+            proj1 (p_forall_ax s R w) e x.
+
+    Definition p_forall_i : forall (s : statterm) (R : (Sns s) -> prop) (p : prop),
+                                (forall x : (Sns s), p entails (R x)) -> p entails (p_forall s R)
+        :=  fun (s : statterm) (R : (Sns s) -> prop) (p : prop)
+                (f : forall x : (Sns s), p entails (R x)) (w : world) (e : (p@w) = true) =>
+            proj2 (p_forall_ax s R w) (fun x : (Sns s) => f x w e).
+
+    Definition p_exists_e : forall (s : statterm) (R : (Sns s) -> prop) (p : prop),
+                                (forall x : (Sns s), (R x) entails p) -> (p_exists s R) entails p
+        :=  fun (s : statterm) (R : (Sns s) -> prop) (p : prop)
+                (g : forall x : (Sns s), (R x) entails p) (w : world) (e : ((p_exists s R)@w) = true) =>
+            (if (p@w) as b return ((p@w) = b -> (p@w) = true)
+             then (fun c : (p@w) = true => c)
+             else (fun d : (p@w) = false =>
+                    False_ind ((p@w) = true)
+                        (proj1 (p_exists_ax s R w) e
+                            (fun x : (Sns s) =>
+                                (if ((R x)@w) as t return (((R x)@w) = t -> ((R x)@w) = false)
+                                 then (fun y : ((R x)@w) = true => False_ind (((R x)@w) = false) (tnf (eq_trans' (g x w y) d)))
+                                 else (fun z : ((R x)@w) = false => z))
+                                eq_refl))))
+            eq_refl.
+
+    Definition p_exists_i : forall (s : statterm) (R : (Sns s) -> prop) (x : (Sns s)), (R x) entails (p_exists s R)
+        :=  fun (s : statterm) (R : (Sns s) -> prop) (x : (Sns s)) (w : world) (e : ((R x)@w) = true) =>
+            proj2 (p_exists_ax s R w) (fun f : forall y : (Sns s), ((R y)@w) = false => tnf (eq_trans' e (f x))).
+
+    (* generalized version of eqw0eqev/neqw0neqev (doesn't require world to be inhabited) *)
+    Definition eqiseqev : forall (s : statterm) (x y : (Sns s)) (u v : world), ((p_equals s x y)@u) = ((p_equals s x y)@v)
+        :=  fun (s : statterm) (x y : (Sns s)) (u v : world) =>
+            (if ((p_equals s x y)@v) as t return (((p_equals s x y)@v) = t -> ((p_equals s x y)@u) = t)
+             then (fun c : ((p_equals s x y)@v) = true => proj2 (p_equals_ax s x y u) (proj1 (p_equals_ax s x y v) c))
+             else (fun d : ((p_equals s x y)@v) = false =>
+                    (if ((p_equals s x y)@u) as b return (((p_equals s x y)@u) = b -> b = false)
+                     then (fun a : ((p_equals s x y)@u) = true =>
+                            eq_trans' (proj2 (p_equals_ax s x y v) (proj1 (p_equals_ax s x y u) a)) d)
+                     else (fun e : ((p_equals s x y)@u) = false => eq_refl))
+                    eq_refl))
+            eq_refl.
+
+    (* These last 3 axioms requires that world is inhabited, specifically by a term w0 *)
+
+    Definition nondeg : ~(truth ≡ falsity)
+        := and_ind (fun (f : truth entails falsity) (g : falsity entails truth) =>
+                        tnf (eq_trans' (f w0 (truth_ax w0)) (falsity_ax w0))).
+
+    Definition eq_one : forall (s : statterm) (x y : (Sns s)), ((p_equals s x y) ≡ truth) \/ ((p_equals s x y) ≡ falsity)
+        :=  fun (s : statterm) (x y : (Sns s)) =>
+            (if ((p_equals s x y)@w0) as b
+             return (((p_equals s x y)@w0) = b -> ((p_equals s x y) ≡ truth) \/ ((p_equals s x y) ≡ falsity))
+             then (fun c : ((p_equals s x y)@w0) = true =>
+                    or_introl   (conj   (truth_top (p_equals s x y))
+                                        (fun (v : world) (e : (truth@v) = true) => eq_trans' (eqiseqev s x y w0 v) c)))
+             else (fun d : ((p_equals s x y)@w0) = false =>
+                    or_intror   (conj   (fun (v : world) (e : ((p_equals s x y)@v) = true) =>
+                                            if (falsity@v) as t return (t = true)
+                                            then eq_refl
+                                            else (eq_trans' d (eq_trans (eqiseqev s x y w0 v) e)))
+                                        (falsity_bot (p_equals s x y)))))
+            eq_refl.
+
+    Definition eq_two : forall (s : statterm) (x y : (Sns s)), ((p_equals s x y) ≡ truth) <-> (x = y)
+        :=  fun (s : statterm) (x y : (Sns s)) =>
+            conj    (and_ind (fun (f : (p_equals s x y) entails truth) (g : truth entails (p_equals s x y)) =>
+                                proj1 (p_equals_ax s x y w0) (g w0 (truth_ax w0))))
+                    (fun e : x = y => conj  (truth_top (p_equals s x y))
+                                            (fun (u : world) (c : (truth@u) = true) => proj2 (p_equals_ax s x y u) e)).
+End prop_Theorems.
+
+(* basically showing that ≡_p implies mutual entailment *)
+Definition int_eq : forall p q : prop, (forall w : world, (p@w) = (q@w)) -> p ≡ q
+    :=  fun (p q : prop) (f : forall w : world, (p @ w) = (q @ w)) =>
+        conj (fun w : world => eq_trans' (f w)) (fun w : world => eq_trans (f w)).
+
+(* duality of prop quantifiers *)
+Definition comp : forall {A B C:Type},(B->C)->(A->B)->A->C := fun (A B C : Type) (f : B -> C) (g : A -> B) (x : A) => f (g x).
+Infix "∘" := comp (at level 20).
+Definition dubneg : forall b : bool, b = -~(-~b) := bool_ind (fun b : bool => b = -~(-~b)) eq_refl eq_refl.
+
+Section QuantifierDuals.
+    Hypotheses (s : statterm) (P : Sns s -> prop).
+    Definition qudupr1 : (p_exists s P) ≡ (not (p_forall s (p_not∘P)))
+        :=  conj    (fun (w : world) (d : ((p_exists s P)@w) = true) =>
+                        eq_trans (p_not_ax (p_forall s (p_not∘P)) w)
+                            (f_equal negb
+                                ((if ((p_forall s (p_not∘P))@w) as b return (((p_forall s (p_not∘P))@w) = b -> b = false)
+                                  then  (fun e : ((p_forall s (p_not∘P))@w) = true =>
+                                            False_ind (true = false)
+                                                (proj1  (p_exists_ax s P w) d
+                                                        (fun x : Sns s =>
+                                                            eq_trans    (dubneg ((P x)@w))
+                                                                        (f_equal negb
+                                                                            (eq_trans' (p_not_ax (P x) w)
+                                                                                (proj1 (p_forall_ax s (p_not∘P) w) e x))))))
+                                  else  (fun _ : ((p_forall s (p_not∘P))@w) = false => eq_refl))
+                                 eq_refl)))
+                    (fun (w : world) (d : (((not p_forall s (p_not∘P)))@w) = true) =>
+                        proj2   (p_exists_ax s P w)
+                                (fun f : forall x : Sns s, (P x @ w) = false =>
+                                    tnf (eq_trans'
+                                            (proj2 (p_forall_ax s (p_not∘P) w)
+                                                (fun x : Sns s => eq_trans (p_not_ax (P x) w) (f_equal negb (f x))))
+                                            (eq_trans (dubneg ((p_forall s (p_not∘P))@w))
+                                                (f_equal negb (eq_trans' (p_not_ax (p_forall s (p_not∘P)) w) d)))))).
+    Definition qudupr2 : (p_forall s P) ≡ (not (p_exists s (p_not∘P)))
+        :=  conj    (fun (w : world) (d : ((p_forall s P)@w) = true) =>
+                        eq_trans (p_not_ax (p_exists s (p_not∘P)) w)
+                            (f_equal negb
+                                ((if ((p_exists s (p_not∘P))@w) as b return ((p_exists s (p_not ∘ P) @ w) = b -> b = false)
+                                  then (fun e : ((p_exists s (p_not∘P))@w) = true =>
+                                            False_ind (true = false)
+                                                (proj1  (p_exists_ax s (p_not∘P) w) e
+                                                        (fun x : Sns s =>
+                                                            eq_trans (p_not_ax (P x) w)
+                                                                (f_equal negb (proj1 (p_forall_ax s P w) d x)))))
+                                  else (fun _ : ((p_exists s (p_not∘P))@w) = false => eq_refl))
+                                 eq_refl)))
+                    (fun (w : world) (d : ((not (p_exists s (p_not∘P)))@w) = true) =>
+                        proj2   (p_forall_ax s P w)
+                                (fun x : Sns s =>
+                                    (if ((P x)@w) as b return (((P x)@w) = b -> b = true)
+                                     then   (fun _ : (P x @ w) = true => eq_refl)
+                                     else   (fun e : (P x @ w) = false =>
+                                                eq_trans'
+                                                    (eq_trans   (dubneg ((p_exists s (p_not∘P))@w))
+                                                                (f_equal negb (eq_trans' (p_not_ax (p_exists s (p_not∘P)) w) d)))
+                                                    (proj2 (p_exists_ax s (p_not∘P) w)
+                                                         (fun f : forall y : Sns s, ((not (P y))@w) = false =>
+                                                          tnf (eq_trans'    (eq_trans (p_not_ax (P x) w) (f_equal negb e))
+                                                                            (f x))))))
+                                    eq_refl)).
+    Definition qudupr3 : (p_exists s (p_not∘P)) ≡ (not (p_forall s P))
+        :=  conj    (fun (w : world) (d : ((p_exists s (p_not∘P))@w) = true) =>
+                        eq_trans (p_not_ax (p_forall s P) w)
+                            (f_equal negb
+                                ((if ((p_forall s P)@w) as b return (((p_forall s P)@w) = b -> b = false)
+                                  then  (fun e : (p_forall s P @ w) = true =>
+                                            False_ind (true = false)
+                                                (proj1 (p_exists_ax s (p_not∘P) w) d
+                                                    (fun x : Sns s =>
+                                                        eq_trans (p_not_ax (P x) w)
+                                                            (f_equal negb (proj1 (p_forall_ax s P w) e x)))))
+                                  else  (fun _ : ((p_forall s P)@w) = false => eq_refl))
+                                 eq_refl)))
+                    (fun (w : world) (d : ((not (p_forall s P))@w) = true) =>
+                        proj2 (p_exists_ax s (p_not∘P) w)
+                            (fun f : forall x : Sns s, ((p_not∘P) x @ w) = false =>
+                                tnf (eq_trans'
+                                        (proj2 (p_forall_ax s P w)
+                                            (fun x : Sns s =>
+                                                eq_trans    (dubneg ((P x)@w))
+                                                            (f_equal negb (eq_trans' (p_not_ax (P x) w) (f x)))))
+                                        (eq_trans   (dubneg ((p_forall s P)@w))
+                                                    (f_equal negb (eq_trans' (p_not_ax (p_forall s P) w) d)))))).
+    Definition qudupr4 : (p_forall s (p_not∘P)) ≡ (not (p_exists s P))
+        := conj     (fun (w : world) (d : ((p_forall s (p_not∘P))@w) = true) =>
+                        eq_trans (p_not_ax (p_exists s P) w)
+                            (f_equal negb
+                                ((if ((p_exists s P)@w) as b return (((p_exists s P)@w) = b -> b = false)
+                                  then  (fun e : ((p_exists s P)@w) = true =>
+                                            False_ind (true = false)
+                                                (proj1 (p_exists_ax s P w) e
+                                                    (fun x : Sns s =>
+                                                        eq_trans (dubneg ((P x)@w))
+                                                            (f_equal negb
+                                                                (eq_trans'  (p_not_ax (P x) w)
+                                                                            (proj1 (p_forall_ax s (p_not∘P) w) d x))))))
+                                  else  (fun _ : ((p_exists s P)@w) = false => eq_refl))
+                                 eq_refl)))
+                    (fun (w : world) (d : ((not (p_exists s P))@w) = true) =>
+                        proj2 (p_forall_ax s (p_not∘P) w)
+                            (fun x : Sns s =>
+                              eq_trans  (p_not_ax (P x) w)
+                                        (f_equal negb
+                                            ((if ((P x)@w) as b return (((P x)@w) = b -> b = false)
+                                              then
+                                              (fun e : ((P x)@w) = true =>
+                                                eq_trans'   (proj2 (p_exists_ax s P w)
+                                                                (fun f : forall y : Sns s, ((P y)@w) = false =>
+                                                                    tnf (eq_trans' e (f x))))
+                                                            (eq_trans   (dubneg ((p_exists s P)@w))
+                                                                        (f_equal negb
+                                                                            (eq_trans' (p_not_ax (p_exists s P) w) d))))
+                                              else  (fun _ : ((P x)@w) = false => eq_refl))
+                                             eq_refl)))).
+End     QuantifierDuals.
+
+
+
+