diff --git a/src/th-bool-dyn/Sidekick_th_bool_dyn.mli b/src/th-bool-dyn/Sidekick_th_bool_dyn.mli
new file mode 100644
index 00000000..d2b03160
--- /dev/null
+++ b/src/th-bool-dyn/Sidekick_th_bool_dyn.mli
@@ -0,0 +1,15 @@
+(** Theory of boolean formulas.
+
+    This handles formulas containing "and", "or", "=>", "if-then-else", etc.
+
+    The difference with {!Sidekick_th_bool_static} is that here, clausification
+    of a formula [F] is done only when [F] is on the trail.
+*)
+
+module Intf = Intf
+module Proof_rules = Proof_rules
+open Intf
+
+module type ARG = Intf.ARG
+
+val theory : (module ARG) -> SMT.Theory.t
diff --git a/src/th-bool-dyn/dune b/src/th-bool-dyn/dune
new file mode 100644
index 00000000..a6a7af8c
--- /dev/null
+++ b/src/th-bool-dyn/dune
@@ -0,0 +1,6 @@
+(library
+ (name Sidekick_th_bool_dyn)
+ (public_name sidekick.th-bool-dyn)
+ (libraries containers sidekick.core sidekick.smt-solver sidekick.util
+   sidekick.simplify)
+ (flags :standard -open Sidekick_util))
diff --git a/src/th-bool-dyn/intf.ml b/src/th-bool-dyn/intf.ml
new file mode 100644
index 00000000..1e36c444
--- /dev/null
+++ b/src/th-bool-dyn/intf.ml
@@ -0,0 +1,29 @@
+open Sidekick_core
+module SMT = Sidekick_smt_solver
+module Simplify = Sidekick_simplify
+
+type term = Term.t
+type ty = Term.t
+
+(** Boolean-oriented view of terms *)
+type 'a bool_view = 'a Bool_view.t =
+  | B_bool of bool
+  | B_not of 'a
+  | B_and of 'a * 'a
+  | B_or of 'a * 'a
+  | B_imply of 'a * 'a
+  | B_equiv of 'a * 'a
+  | B_xor of 'a * 'a
+  | B_eq of 'a * 'a
+  | B_neq of 'a * 'a
+  | B_ite of 'a * 'a * 'a
+  | B_atom of 'a
+
+(** Argument to the theory *)
+module type ARG = sig
+  val view_as_bool : term -> term bool_view
+  (** Project the term into the boolean view. *)
+
+  val mk_bool : Term.store -> term bool_view -> term
+  (** Make a term from the given boolean view. *)
+end
diff --git a/src/th-bool-dyn/proof_rules.ml b/src/th-bool-dyn/proof_rules.ml
new file mode 100644
index 00000000..82288385
--- /dev/null
+++ b/src/th-bool-dyn/proof_rules.ml
@@ -0,0 +1,19 @@
+open Sidekick_core
+
+type term = Term.t
+type lit = Lit.t
+
+let lemma_bool_tauto lits : Proof_term.t =
+  Proof_term.apply_rule "bool.tauto" ~lits
+
+let lemma_bool_c name terms : Proof_term.t =
+  Proof_term.apply_rule ("bool.c." ^ name) ~terms
+
+let lemma_bool_equiv t u : Proof_term.t =
+  Proof_term.apply_rule "bool.equiv" ~terms:[ t; u ]
+
+let lemma_ite_true ~ite : Proof_term.t =
+  Proof_term.apply_rule "bool.ite.true" ~terms:[ ite ]
+
+let lemma_ite_false ~ite : Proof_term.t =
+  Proof_term.apply_rule "bool.ite.false" ~terms:[ ite ]
diff --git a/src/th-bool-dyn/proof_rules.mli b/src/th-bool-dyn/proof_rules.mli
new file mode 100644
index 00000000..0379b4c5
--- /dev/null
+++ b/src/th-bool-dyn/proof_rules.mli
@@ -0,0 +1,20 @@
+open Sidekick_core
+
+type term = Term.t
+type lit = Lit.t
+
+val lemma_bool_tauto : lit list -> Proof_term.t
+(** Boolean tautology lemma (clause) *)
+
+val lemma_bool_c : string -> term list -> Proof_term.t
+(** Basic boolean logic lemma for a clause [|- c].
+      [proof_bool_c b name cs] is the Proof_term.t designated by [name]. *)
+
+val lemma_bool_equiv : term -> term -> Proof_term.t
+(** Boolean tautology lemma (equivalence) *)
+
+val lemma_ite_true : ite:term -> Proof_term.t
+(** lemma [a ==> ite a b c = b] *)
+
+val lemma_ite_false : ite:term -> Proof_term.t
+(** lemma [¬a ==> ite a b c = c] *)