diff --git a/CHANGES.md b/CHANGES.md
index 783f6da8e..9e388e5ca 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -22,6 +22,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Tactic `#print` to print a symbol or the current goal.
 - Export to Lean.
 - Tactic `all_hyps t` calls parameterized tactic term t on all hypotheses ignoring failing calls.
+- Conditional rules `l when t1 ≡ t2 ↪ r`
 
 ### Changed
 
diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf
index 57b19e549..71c2efe43 100644
--- a/doc/lambdapi.bnf
+++ b/doc/lambdapi.bnf
@@ -33,6 +33,10 @@
 <constructor> ::= <uid> <param_list>* ":" <term>
 
 <rule> ::= <term> "↪" <term>
+         | <term> when <condition> "↪" <term>
+
+<condition> ::= <term> ≡ <term>
+              | <term> «[<term>] <term>
 
 <unif_rule> ::= <equation> "↪" "[" <equation> (";" <equation>)* "]"
 
diff --git a/editors/emacs/lambdapi-smie.el b/editors/emacs/lambdapi-smie.el
index 2b9ad2b30..c004074a2 100644
--- a/editors/emacs/lambdapi-smie.el
+++ b/editors/emacs/lambdapi-smie.el
@@ -56,7 +56,8 @@
      "rule"
      "symbol"
      "unif_rule"
-     "verbose")
+     "verbose"
+     "when")
    lambdapi--queries)
   "Commands at top level.")
 
@@ -142,7 +143,9 @@ Indent by `lambdapi-indent-basic' in proofs, and 0 otherwise."
       (symdec ("symbol" args ":" sterm))
       (indcons (args ":" sterm) ("|" args ":" sterm))
       (inddec (inddec "with" args ":" sterm "≔" indcons))
-      (rules (rules "with" sterm "↪" sterm))
+      (rules (rules "with" sterm "↪" sterm)
+             (rules "with" sterm "when" condition "↪" sterm))
+      (condition (sterm "«[" sterm "]" sterm) (sterm "≡" sterm))
       (command
                ("begin" prfcontent "abort" ";")
                ("begin" prfcontent "admitted" ";")
@@ -240,7 +243,7 @@ The default lexer is used because the syntax is primarily made of sexps."
                       "print" "proofterm" "search" "type"))
      (lambdapi--query-indent))
 
-    (`(,_ . ,(or "," "↪" "→" "≡")) (smie-rule-separator kind))
+    (`(,_ . ,(or "«" "," "↪" "→" "≡")) (smie-rule-separator kind))
 
     (`(,(or :before :list-intro) . ,(or "≔" ":")) (smie-rule-separator kind))
     (`(:after . ,(or "≔" ":")) lambdapi-indent-basic)
diff --git a/editors/emacs/lambdapi-vars.el b/editors/emacs/lambdapi-vars.el
index d5f54afdb..57513f00c 100644
--- a/editors/emacs/lambdapi-vars.el
+++ b/editors/emacs/lambdapi-vars.el
@@ -47,6 +47,7 @@
     "rule"
     "symbol"
     "unif_rule"
+    "when"
     "with")
   "Commands that enrich the signature.")
 
@@ -106,6 +107,7 @@
     (modify-syntax-entry ?→ "." table)
     (modify-syntax-entry ?↪ "." table)
     (modify-syntax-entry ?≔ "." table)
+    (modify-syntax-entry ?« "." table)
     (modify-syntax-entry ?$ "." table)
     (modify-syntax-entry ?? "." table)
     (modify-syntax-entry ?: "." table)
diff --git a/editors/vim/syntax/lambdapi.vim b/editors/vim/syntax/lambdapi.vim
index 4e485eb42..5c1635815 100644
--- a/editors/vim/syntax/lambdapi.vim
+++ b/editors/vim/syntax/lambdapi.vim
@@ -98,6 +98,7 @@ syntax keyword KeywordOK contained type
 syntax keyword KeywordOK contained TYPE
 syntax keyword KeywordOK contained unif_rule
 syntax keyword KeywordOK contained verbose
+syntax keyword KeywordOK contained when
 syntax keyword KeywordOK contained why3
 syntax keyword KeywordOK contained with
 highlight link KeywordOK Keyword
@@ -172,6 +173,7 @@ syntax keyword KeywordKO contained type
 syntax keyword KeywordKO contained TYPE
 syntax keyword KeywordKO contained unif_rule
 syntax keyword KeywordKO contained verbose
+syntax keyword KeywordKO contained when
 syntax keyword KeywordKO contained why3
 syntax keyword KeywordKO contained with
 highlight link KeywordKO Error
@@ -207,6 +209,7 @@ syntax match Keyword ","
 syntax match Keyword ";"
 syntax match Keyword "_"
 syntax match Keyword "≡"
+syntax match Keyword "«"
 
 " Other special classes.
 syntax match Type "\u\w*"
@@ -215,6 +218,7 @@ syntax match PreProc  "?\(\<\h\w*\>\|\({|\([^|]\|\(|[^}]\)\)*|*|}\)\)"
 
 " Abbreviations.
 abbreviate --> ↪
+abbreviate << «
 abbreviate -> →
 abbreviate => ⇒
 abbreviate !  Π
diff --git a/editors/vscode/syntaxes/lp.tmLanguage.json b/editors/vscode/syntaxes/lp.tmLanguage.json
index e7a25f740..bbf5d44ff 100644
--- a/editors/vscode/syntaxes/lp.tmLanguage.json
+++ b/editors/vscode/syntaxes/lp.tmLanguage.json
@@ -45,7 +45,7 @@
     },
 
     "signature-commands": {
-      "match": "(coerce_rule|inductive|rule|symbol|unif_rule|with)\\s+([^\\s+]*)",
+      "match": "(coerce_rule|inductive|rule|symbol|unif_rule|with|when)\\s+([^\\s+]*)",
       "captures": {
         "1": {"name": "storage.type.lp"},
         "2": {"name": "entity.name.function.theorem.lp"}
diff --git a/misc/lambdapi.tex b/misc/lambdapi.tex
index 02d29e67b..7b4f739ad 100644
--- a/misc/lambdapi.tex
+++ b/misc/lambdapi.tex
@@ -9,7 +9,7 @@
   tabsize=2,
   basicstyle={\ttfamily\small\upshape},
   backgroundcolor=\color{lightgrey},
-  keywords={abort,admit,admitted,all_hyps,apply,as,assert,assertnot,associative,assume,assumption,begin,builtin,change,commutative,compute,constant,debug,end,eval,fail,flag,first_hyp,focus,generalize,have,in,induction,inductive,infix,injective,left,let,notation,off,on,opaque,open,orelse,prefix,print,private,proofterm,protected,prover,prover_timeout,quantifier,refine,reflexivity,repeat,require,rewrite,right,rule,sequential,set,simplify,solve,symbol,symmetry,type,TYPE,unif_rule,verbose,why3,with},
+  keywords={abort,admit,admitted,all_hyps,apply,as,assert,assertnot,associative,assume,assumption,begin,builtin,change,commutative,compute,constant,debug,end,eval,fail,flag,first_hyp,focus,generalize,have,in,induction,inductive,infix,injective,left,let,notation,off,on,opaque,open,orelse,prefix,print,private,proofterm,protected,prover,prover_timeout,quantifier,refine,reflexivity,repeat,require,rewrite,right,rule,sequential,set,simplify,solve,symbol,symmetry,type,TYPE,unif_rule,verbose,why3,with,when},
   sensitive=true,
   keywordstyle=\color{blue},
   morecomment=[l]{//},
@@ -26,6 +26,7 @@
   {≔}{$\coloneqq$}1
   {⊢}{$\vdash$}1
   {≡}{$\equiv$}1
+  {«}{$\ll$}1
   {𝔹}{$\mathbb{B}$}1
   {𝕃}{$\mathbb{L}$}1
   {ℕ}{$\mathbb{N}$}1
diff --git a/src/core/coercion.ml b/src/core/coercion.ml
index 3faf8bb5b..7cc708ecc 100644
--- a/src/core/coercion.ml
+++ b/src/core/coercion.ml
@@ -15,6 +15,6 @@ let _ =
     and t = mk_Patt (Some 1, "t", [||]) in
     let lhs = [a;a;t] and arities = [|0;0|] and names = [|"A";"t"|] in
     { lhs; names; rhs=t; arity=3; arities; vars_nb=2; xvars_nb = 0;
-      rule_pos = None }
+      rule_pos = None; r_when = R_None }
   in
   Sign.add_rule Ghost.sign (coerce, rule)
diff --git a/src/core/eval.ml b/src/core/eval.ml
index 0eaf29c56..68ba96f52 100644
--- a/src/core/eval.ml
+++ b/src/core/eval.ml
@@ -342,6 +342,33 @@ and tree_walk : config -> sym -> stack -> (term * stack) option =
               let vi = Array.map (fun id -> mk_Vari (var id)) vi in
               let tj = msubst bj vi in
               if eq_modulo whnf cfg vars.(i) tj then ok else fail
+          | CondEQ(((p1,o1) as op1,a1), ((p2,o2) as op2,a2)) ->
+              let v1 = List.map (fun (i,_) -> vars.(i)) a1 in
+              let v2 = List.map (fun (i,_) -> vars.(i)) a2 in
+              if Logger.log_enabled() then
+                log_rew "%aCondEQ(%s[%a],%s[%a]) : %s(%a) == %s(%a)"
+                  D.depth !depth
+                  (snd op1) (List.pp D.int ",") (List.map fst a1)
+                  (snd op2) (List.pp D.int ",") (List.map fst a2)
+                  (snd op1) (List.pp Raw.term ",") v1
+                  (snd op2) (List.pp Raw.term ",") v2;
+              let s1 = Sign.find_qualified p1 o1 in
+              let s2 = Sign.find_qualified p2 o2 in
+              let t1 = add_args (mk_Symb s1) v1 in
+              let t2 = add_args (mk_Symb s2) v2 in
+              if eq_modulo whnf cfg t1 t2 then ok else fail
+          | CondST((pth,op), p1, p2) ->
+              let v1 = vars.(fst p1) and v2 = vars.(fst p2) in
+              if Logger.log_enabled() then
+                log_rew "%aCondST(%s,%d,%d) : %a <<[%s] %a"
+                  D.depth !depth
+                  op (fst p1) (fst p2) Raw.term v1 op Raw.term v2;
+              let rec find (p: term -> bool) (t: term) =
+                match unfold t with
+                | Appl(Appl(Symb s,a1), a2)
+                     when s.sym_path=pth && s.sym_name=op -> p a1 || find p a2
+                | t -> p t in
+              if find (eq_modulo whnf cfg v1) v2 then ok else fail
           | CondFV(i,xs) ->
               let allowed =
                 (* Variables that are allowed in the term. *)
diff --git a/src/core/term.ml b/src/core/term.ml
index 1791c8b57..472a3f056 100644
--- a/src/core/term.ml
+++ b/src/core/term.ml
@@ -206,6 +206,14 @@ and sym =
 
 (** {3 Representation of rewriting rules} *)
 
+(** optional rule constraints *)
+and r_constraint =
+  (* equality constraint f p1 ... pn == g q1 ... qm *)
+  | R_EQ of (sym * int list) * (sym * int list)
+  (* subterm constraint p <<[op] q *)
+  | R_ST of sym * int * int
+  | R_None (* no constraint *)
+
 (** Representation of a rewriting rule. A rewriting rule is mainly formed of a
     LHS (left hand side),  which is the pattern that should be matched for the
     rule to apply, and a RHS (right hand side) giving the action to perform if
@@ -214,6 +222,7 @@ and sym =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
+  ; r_when   : r_constraint (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
diff --git a/src/core/term.mli b/src/core/term.mli
index 5af110b65..32bb0eb6e 100644
--- a/src/core/term.mli
+++ b/src/core/term.mli
@@ -138,6 +138,14 @@ and sym =
 
 (** {3 Representation of rewriting rules} *)
 
+(** optional rule constraints *)
+and r_constraint =
+  (* equality constraint f p1 ... pn == g q1 ... qm *)
+  | R_EQ of (sym * int list) * (sym * int list)
+  (* subterm constraint p <<[op] q *)
+  | R_ST of sym * int * int
+  | R_None (* no constraint *)
+
 (** Representation of a rewriting rule. A rewriting rule is mainly formed of a
     LHS (left hand side),  which is the pattern that should be matched for the
     rule to apply, and a RHS (right hand side) giving the action to perform if
@@ -146,6 +154,7 @@ and rule =
   { lhs      : term list (** Left hand side (LHS). *)
   ; names    : string array (** Names of pattern variables. *)
   ; rhs      : term (** Right hand side (RHS). *)
+  ; r_when   : r_constraint (** conditional rule constraint. *)
   ; arity    : int (** Required number of arguments to be applicable. *)
   ; arities  : int array
   (** Arities of the pattern variables bound in the RHS. *)
@@ -175,8 +184,8 @@ and rule =
        concrete syntax) are represented in the same way, and with a unique
        name (in the rule) that is generated automatically.
 
-    Then, the term [f t u v w] matches the LHS with a substitution represented
-    by an array of terms [a] of length 3 if we
+    Then, the term [f t u v w] matches the LHS with a substitution
+    represented by an array of terms [a] of length 3 if we
     have [a.(0) = t], [a.(1) = u], [a.(1) = v] and [a.(2) = w].
 
     {b TODO} memorising [w] in the substitution is sub-optimal. In practice,
diff --git a/src/core/tree.ml b/src/core/tree.ml
index dfbe2190e..e1c12d7a7 100644
--- a/src/core/tree.ml
+++ b/src/core/tree.ml
@@ -71,6 +71,20 @@ module CP = struct
       let compare = Stdlib.compare
     end)
 
+  (** Functional sets of pairs of flat terms. *)
+  module TSet = Set.Make(
+    struct
+      type t = (psym * pvar list) * (psym * pvar list)
+      let compare = Stdlib.compare
+    end)
+
+  (** Functional sets of subterm constraints. *)
+  module STSet = Set.Make(
+    struct
+      type t = psym * pvar * pvar
+      let compare = Stdlib.compare
+    end)
+
   (** A pool of (convertibility and free variable) conditions. *)
   type t =
     { variables : pvar IntMap.t
@@ -85,17 +99,27 @@ module CP = struct
     ; fv_conds : int array IntMap.t
     (** A mapping of [i] to [xs] represents a free variable condition that can
         only be satisfied if only the free variables of [x] appear in the term
-        stored at slot [i] in the [vars] array of [Eval.tree_walk]. *) }
+        stored at slot [i] in the [vars] array of [Eval.tree_walk]. *)
+    ; eq_conds : TSet.t
+    (** Set of pairs of terms that should be convertible. *)
+    ; st_conds : STSet.t
+    (** sets of subterm constraints. *)
+    }
 
   (** [empty] is the condition pool holding no condition. *)
   let empty : t =
     { variables = IntMap.empty
     ; nl_conds = PSet.empty
-    ; fv_conds = IntMap.empty }
+    ; fv_conds = IntMap.empty
+    ; eq_conds = TSet.empty
+    ; st_conds = STSet.empty }
 
   (** [is_empty pool] tells whether the pool of constraints is empty. *)
   let is_empty : t -> bool = fun pool ->
-    PSet.is_empty pool.nl_conds && IntMap.is_empty pool.fv_conds
+    PSet.is_empty pool.nl_conds
+    && IntMap.is_empty pool.fv_conds
+    && TSet.is_empty pool.eq_conds
+    && STSet.is_empty pool.st_conds
 
   (** [register_nl i (slot,vs) pool] registers the fact that the slot [slot]
       in the [vars] array correspond to a term stored at index [i] in the
@@ -119,6 +143,20 @@ module CP = struct
   let register_fv : int -> int array -> t -> t = fun i vs pool ->
     { pool with fv_conds = IntMap.add i vs pool.fv_conds }
 
+  (** [register_eq t1 t2 pool] registers a convertibility constraint
+      between terms [t1] and [t2] in [pool]. *)
+  let register_eq : (psym * int list) -> (psym * int list) -> t -> t =
+    fun (s1,a1) (s2,a2) pool ->
+    let pv1 = List.map (fun i -> IntMap.find i pool.variables) a1 in
+    let pv2 = List.map (fun i -> IntMap.find i pool.variables) a2 in
+    { pool with eq_conds = TSet.add ((s1,pv1),(s2,pv2)) pool.eq_conds }
+
+  let register_st : psym -> int -> int -> t -> t =
+    fun op i j pool ->
+    let pv1 = IntMap.find i pool.variables in
+    let pv2 = IntMap.find j pool.variables in
+    { pool with st_conds = STSet.add (op, pv1, pv2) pool.st_conds }
+
   (** [constrained_nl i pool] tells whether index [i] in the RHS's environment
       has already been associated to a variable of the [vars] array. *)
   let constrained_nl : int -> t -> bool = fun slot pool ->
@@ -129,6 +167,9 @@ module CP = struct
   let is_contained : tree_cond -> t -> bool = fun cond pool ->
     match cond with
     | CondNL(i,j) -> PSet.mem (i,j) pool.nl_conds
+    | CondEQ(t1,t2) -> TSet.mem (t1,t2) pool.eq_conds
+                       || TSet.mem (t2,t1) pool.eq_conds
+    | CondST(o,t1,t2) -> STSet.mem (o,t1,t2) pool.st_conds
     | CondFV(i,x) ->
         try Array.eq (=) x (IntMap.find i pool.fv_conds)
         with Not_found -> false
@@ -137,6 +178,9 @@ module CP = struct
   let remove cond pool =
     match cond with
     | CondNL(i,j)  -> {pool with nl_conds = PSet.remove (i,j) pool.nl_conds}
+    | CondEQ(t,u) -> {pool with eq_conds = TSet.remove (t,u) pool.eq_conds}
+    | CondST(o,t,u) ->
+        {pool with st_conds = STSet.remove (o,t,u) pool.st_conds}
     | CondFV(i,xs) ->
         try
           let ys = IntMap.find i pool.fv_conds in
@@ -161,8 +205,28 @@ module CP = struct
       | p :: ps -> try Some(export (IntMap.choose p.fv_conds))
                    with Not_found -> choose_vf ps
     in
+    let rec choose_eq pools =
+      let export (t1, t2) = CondEQ(t1,t2) in
+      match pools with
+      | []      -> None
+      | p :: ps -> try Some(export (TSet.choose p.eq_conds))
+                   with Not_found -> choose_eq ps
+    in
+    let rec choose_st pools =
+      let export (op, t1, t2) = CondST(op,t1,t2) in
+      match pools with
+      | []      -> None
+      | p :: ps -> try Some(export (STSet.choose p.st_conds))
+                   with Not_found -> choose_st ps
+    in
     let res = choose_nl pools in
-    if res = None then choose_vf pools else res
+    if res = None then
+      let res = choose_eq pools in
+      if res = None then
+        let res = choose_st pools in
+        if res = None then choose_vf pools else res
+      else res
+    else res
 end
 
 (** {1 Clause matrix and pattern matching problem} *)
@@ -218,12 +282,23 @@ module CM = struct
       [0] index is used when going under abstractions. In that case, the field
       [arg_rank] is incremented. *)
 
+  (** rule constraints *)
+  type c_constraint =
+    | C_EQ of (psym * int list) * (psym * int list)
+    (** convertibility between flat terms *)
+    | C_ST of psym * int * int
+    (** subterm constraint between pattern variables *)
+    | C_None
+    (** no cnostraint *)
+
   (** A clause matrix row (schematically {i c_lhs ↪ c_rhs if cond_pool}). *)
   type clause =
     { c_lhs       : term array
     (** Left hand side of a rule. *)
     ; c_rhs       : rule
     (** Right hand side of a rule, and number of extra variables. *)
+    ; c_when      : c_constraint
+    (** constraints for conditional rules *)
     ; c_subst     : rhs_substit
     (** Substitution of RHS variables. *)
     ; xvars_nb    : int
@@ -290,9 +365,16 @@ module CM = struct
 
   (** [of_rules rs] transforms rewriting rules [rs] into a clause matrix. *)
   let of_rules : rule list -> t = fun rs ->
-    let r2r ({lhs; xvars_nb; _} as c_rhs) =
+    let r2r ({lhs; xvars_nb; r_when; _} as c_rhs) =
       let c_lhs = Array.of_list lhs in
-      { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb }
+      let c_when = match r_when with
+        | R_None -> C_None
+        | R_EQ ((s1,a1),(s2,a2)) ->
+            C_EQ (((s1.sym_path,s1.sym_name), a1),
+                  ((s2.sym_path,s2.sym_name), a2))
+        | R_ST (op,p,q) -> C_ST ((op.sym_path,op.sym_name), p, q)
+      in
+      { c_lhs; c_rhs; cond_pool = CP.empty; c_subst = []; xvars_nb; c_when }
     in
     let size = (* Get length of longest rule *)
       if rs = [] then 0 else
@@ -357,7 +439,7 @@ module CM = struct
   (** [is_exhausted p c] tells whether clause [r] whose terms are at positions
       in [p] can be applied or not. *)
   let is_exhausted : arg list -> clause -> bool =
-    fun positions {c_lhs = lhs ; cond_pool ; _} ->
+    fun positions {c_lhs = lhs ; cond_pool ; c_when; _} ->
     let nonl lhs =
       (* Verify that there are no non linearity constraints in the remaining
          terms.  We must check that there are no constraints in the remaining
@@ -384,7 +466,7 @@ module CM = struct
       in
       Array.for_all2 check lhs de && nonl lhs
     in
-    CP.is_empty cond_pool && (lhs = [||] || ripe lhs)
+    c_when = C_None && CP.is_empty cond_pool && (lhs = [||] || ripe lhs)
 
   (** [yield m] returns the next operation to carry out on matrix [m], that
       is, either specialising, solving a constraint or rewriting to a rule. *)
@@ -482,6 +564,32 @@ module CM = struct
               CP.register_nl i (mem,vs) cond_pool
           | None    -> cond_pool
         in
+        let c_when, cond_pool =
+          let vars = cond_pool.variables in
+          match r.c_rhs.r_when with
+          | R_None -> r.c_when, cond_pool
+          | R_ST (sy, i, j) when
+                 IntMap.mem i vars && IntMap.mem j vars ->
+              if Logger.log_enabled () then
+                log "Registering subterm constraint on position [%a] \
+                     %d <<[%s] %d"
+                  arg_path a.arg_path i sy.sym_name j;
+              C_None, CP.register_st (sy.sym_path,sy.sym_name) i j cond_pool
+          | R_EQ ((op1,a1), (op2,a2)) when
+                 List.for_all (fun i -> IntMap.mem i vars) a1
+                 && List.for_all (fun i -> IntMap.mem i vars) a2 ->
+              if Logger.log_enabled () then
+                log "Registering user constraint on position [%a] \
+                     %s %a == %s %a"
+                  arg_path a.arg_path
+                  op1.sym_name (List.pp int " ") a1
+                  op2.sym_name (List.pp int " ") a2;
+              C_None, CP.register_eq
+                      ((op1.sym_path,op1.sym_name), a1)
+                      ((op2.sym_path,op2.sym_name), a2)
+                      cond_pool
+          | _ -> r.c_when, cond_pool
+        in
         let c_subst =
           (* REVIEW: patterns may have slots in the RHS although they are not
              bound. *)
@@ -499,7 +607,7 @@ module CM = struct
               (mem, (i,vs)) :: r.c_subst
           | _ -> r.c_subst
         in
-        {r with c_subst; cond_pool}
+        {r with c_subst; cond_pool; c_when}
     | _ -> r
 
   (** [specialize free_vars pat col pos cls] filters and transforms LHS of
diff --git a/src/core/tree_type.ml b/src/core/tree_type.ml
index c2d7d17a2..89933a92f 100644
--- a/src/core/tree_type.ml
+++ b/src/core/tree_type.ml
@@ -6,6 +6,7 @@ open Common
 (** {3 Atomic pattern constructor representation} *)
 
 type pvar = int * int array
+type psym = Path.t * string
 
 (** Representation of an atomic pattern constructor. *)
 module TC =
@@ -56,6 +57,11 @@ type tree_cond =
   | CondFV of pvar
   (** Are the (indexed) bound variables (which are free at the time of the
       checking) of the term at the given index in the array? *)
+  | CondEQ of (psym * pvar list) * (psym * pvar list)
+  (** user rule condition: are the two terms equivalent *)
+  | CondST of psym * pvar * pvar
+  (** user rule condition: is the 1st pvar a subterm of the 2nd while
+   traversing psym calls *)
 
 (** {b NOTE} that when performing a [tree_cond.CondFV] check, we
     are concerned about variables that were bound in the term being reduced
@@ -69,6 +75,11 @@ let tree_cond : tree_cond pp = fun ppf tc ->
       out ppf "Nl(%d[%a],%d[%a])"
         i (Array.pp int ",") xs j (Array.pp int ",") ys
   | CondFV(i, _) -> out ppf "Fv(%d)" i
+  | CondEQ((s1,a1), (s2,a2)) ->
+      out ppf "Eq(%s(%a),%s(%a))"
+        (snd s1) (List.pp int ",") (List.map fst a1)
+        (snd s2) (List.pp int ",") (List.map fst a2)
+  | CondST(op,p,q) -> out ppf "St(%s,%d,%d)" (snd op) (fst p) (fst q)
 
 (** Substitution of variables in a RHS. During the filtering process, some
     subterms of the filtered term may be stored in an array. Let [v] be that
diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml
index b9b917e67..d39d350dd 100644
--- a/src/export/rawdk.ml
+++ b/src/export/rawdk.ml
@@ -135,9 +135,12 @@ let rec remove_wraps ({elt;_} as t) =
 
 let rule : p_rule pp =
   let varset ppf set = List.pp string ", " ppf (StrSet.elements set) in
-  fun ppf {elt=(l,r);_} ->
-  out ppf "[%a] %a --> %a.@."
-    varset (pvars_lhs l) term (remove_wraps l) term r
+  fun ppf {elt=(l,r,w);_} ->
+  if w = P_None then
+    out ppf "[%a] %a --> %a.@."
+      varset (pvars_lhs l) term (remove_wraps l) term r
+  else
+    fatal None "Cannot translate conditional rules."
 
 type modifiers
   = prop list * expo list * match_strat list * p_modifier_aux list
diff --git a/src/handle/inductive.ml b/src/handle/inductive.ml
index ff2eaa2bd..57c15b97f 100644
--- a/src/handle/inductive.ml
+++ b/src/handle/inductive.ml
@@ -347,7 +347,7 @@ let iter_rec_rules :
     let nonrec_dom _ _ next = next in
     let codom xs rhs _ ts =
       let cons_arg = P.appl_list (P.iden cons_sym.sym_name) (List.rev xs) in
-      Pos.make rules_pos (arec ind_sym ts cons_arg, rhs)
+      Pos.make rules_pos (arec ind_sym ts cons_arg, rhs, P_None)
     in
     fold_cons_type pos ind_pred_map "" ind_sym vs cons_sym inj_var
       init aux acc_rec_dom rec_dom acc_nonrec_dom nonrec_dom codom
diff --git a/src/parsing/dkRule.ml b/src/parsing/dkRule.ml
index 09d709a20..135420c42 100644
--- a/src/parsing/dkRule.ml
+++ b/src/parsing/dkRule.ml
@@ -155,4 +155,4 @@ let to_p_rule : p_dk_rule -> p_rule = fun r ->
   (* NOTE the computation order is important for setting arities properly. *)
   let lhs = build [] lhs in
   let rhs = build [] rhs in
-  Pos.make r.pos (lhs, rhs)
+  Pos.make r.pos (lhs, rhs, P_None)
diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml
index 2693b5791..275284dab 100644
--- a/src/parsing/lpLexer.ml
+++ b/src/parsing/lpLexer.ml
@@ -100,6 +100,7 @@ type token =
   | TYPE_TERM
   | UNIF_RULE
   | VERBOSE
+  | WHEN
   | WHY3
   | WITH
 
@@ -134,6 +135,7 @@ type token =
   | R_PAREN
   | R_SQ_BRACKET
   | SEMICOLON
+  | SUBTERM
   | THICKARROW (* only in Rocq *)
   | TURNSTILE
   | UNDERSCORE
@@ -306,6 +308,7 @@ let rec token ~allow_rocq_syntax lb =
   | "TYPE" -> TYPE_TERM
   | "unif_rule" -> UNIF_RULE
   | "verbose" -> VERBOSE
+  | "when" -> WHEN
   | "why3" -> WHY3
   | "with" -> WITH
 
@@ -336,6 +339,7 @@ let rec token ~allow_rocq_syntax lb =
   | ')' -> R_PAREN
   | ']' -> R_SQ_BRACKET
   | ';' -> SEMICOLON
+  | 0xab (* « *) -> SUBTERM
   | 0x22a2 (* ⊢ *) -> TURNSTILE
   | '|' -> VBAR
   | '_' -> UNDERSCORE
diff --git a/src/parsing/lpParser.ml b/src/parsing/lpParser.ml
index 3bdd29d4c..c48ccaa80 100644
--- a/src/parsing/lpParser.ml
+++ b/src/parsing/lpParser.ml
@@ -99,6 +99,7 @@ let string_of_token = function
   | SIMPLIFY -> "simplify"
   | SOLVE -> "solve"
   | STRINGLIT _ -> "string literal"
+  | SUBTERM -> "«"
   | SWITCH false -> "off"
   | SWITCH true -> "on or off"
   | SYMBOL -> "symbol"
@@ -116,6 +117,7 @@ let string_of_token = function
   | UNIF_RULE -> "unif_rule"
   | VBAR -> "|"
   | VERBOSE -> "verbose"
+  | WHEN -> "when"
   | WHY3 -> "why3"
   | WITH -> "with"
 
@@ -597,7 +599,7 @@ and command (lb:'token lexbuf) : p_command =
         let (en, es) = List.(hd es, tl es) in
         let cat e es = P.appl (P.appl cons e) es in
         let rhs = List.fold_right cat es en in
-        let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs) in
+        let r = extend_pos lb (*__FUNCTION__*) pos1 (lhs, rhs, P_None) in
         extend_pos lb (*__FUNCTION__*) pos1 (P_unif_rule(r))
     | COERCE_RULE ->
         consume_token lb;
@@ -753,13 +755,33 @@ and notation (lb:'token lexbuf): string Term.notation =
       expected lb "" [INFIX;POSTFIX;PREFIX;QUANTIFIER]
 
 and rule_tks () = term_tks
-and rule (lb:'token lexbuf): (p_term * p_term) loc =
+and rule (lb:'token lexbuf):
+      (p_term * p_term * p_constraint) loc =
   if log_enabled() then log "%s" __FUNCTION__;
   let pos1 = current_pos lb in
   let l = term lb in
+  let w =
+    if (current_token lb == WHEN) then begin
+        consume WHEN lb;
+        let t1 = term lb in
+        if (current_token lb == EQUIV) then begin
+            consume EQUIV lb;
+            let t2 = term lb in
+            P_EQ(t1, t2)
+          end
+        else begin
+            consume SUBTERM lb;
+            consume L_SQ_BRACKET lb;
+            let op = term lb in
+            consume R_SQ_BRACKET lb;
+            let t2 = term lb in
+            P_ST (op,t1,t2)
+          end
+      end
+    else P_None in
   consume HOOK_ARROW lb;
   let r = term lb in
-  extend_pos lb (*__FUNCTION__*) pos1 (l, r)
+  extend_pos lb (*__FUNCTION__*) pos1 (l, r, w)
 
 and equation_tks () = term_tks
 and equation (lb:'token lexbuf): p_term * p_term =
diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml
index 6a1b790f0..299a57edf 100644
--- a/src/parsing/pretty.ml
+++ b/src/parsing/pretty.ml
@@ -187,8 +187,13 @@ and params_list : p_params list pp = fun ppf ->
 and typ : p_term option pp = fun ppf t ->
   Option.iter (out ppf "@ : %a" term) t
 
-let rule : string -> p_rule pp = fun kw ppf {elt=(l,r);_} ->
-  out ppf "%s %a ↪ %a" kw term l term r
+let rule : string -> p_rule pp = fun kw ppf {elt=(l,r,w);_} ->
+  match w with
+  | P_None -> out ppf "%s %a ↪ %a" kw term l term r
+  | P_EQ (t1,t2) -> out ppf "%s %a when %a ≡ %a ↪ %a"
+                      kw term l term t1 term t2 term r
+  | P_ST (o,t1,t2) -> out ppf "%s %a when %a «[%a] %a ↪ %a"
+                      kw term l term t1 term o term t2 term r
 
 let inductive : string -> p_inductive pp =
   let cons ppf (id,a) = out ppf "@,| %a : %a" ident id term a in
@@ -214,7 +219,7 @@ let rec unpack : p_term -> (p_term * p_term) list = fun eqs ->
       else assert false
   | _ -> assert false
 
-let unif_rule : p_rule pp = fun ppf {elt=(l,r);_} ->
+let unif_rule : p_rule pp = fun ppf {elt=(l,r,_);_} ->
   let lhs =
     match Syntax.p_get_args l with
     | (_, [t; u]) -> (t, u)
diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml
index def6973a5..48fdd2e81 100644
--- a/src/parsing/scope.ml
+++ b/src/parsing/scope.ml
@@ -547,13 +547,22 @@ let patt_vars : p_term -> (string * int) list * string list =
 let scope_rule :
   ?find_sym:find_sym -> bool -> sig_state -> p_rule -> sym_rule =
   fun ?(find_sym=Sig_state.find_sym) ur ss
-      { elt = (p_lhs, p_rhs); pos = rule_pos} ->
+      { elt = (p_lhs, p_rhs, p_when); pos = rule_pos} ->
   (* Compute the set of pattern variables on both sides. *)
   let (pvs_lhs, nl) = patt_vars p_lhs in
   (* NOTE to reject non-left-linear rules check [nl = []] here. *)
   let (pvs_rhs, _ ) = patt_vars p_rhs in
   (* Check that pattern variables of RHS that are in the LHS have the right
      arity. *)
+  let pvs_when =
+    match p_when with
+    | P_None -> []
+    | P_EQ (t1,t2) ->
+        let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in
+        p1 @ p2
+    | P_ST (_o,t1,t2) ->
+        let (p1,_) = patt_vars t1 and (p2,_) = patt_vars t2 in
+        p1 @ p2 in
   let check_arity (m,i) =
     try
       let j = List.assoc m pvs_lhs in
@@ -561,6 +570,7 @@ let scope_rule :
     with Not_found -> ()
   in
   List.iter check_arity pvs_rhs;
+  List.iter check_arity pvs_when;
   (* [get_root t] returns the symbol at the root of the p_term [t]. *)
   let rec get_root t = get_root_after_pratt (Pratt.parse ~find_sym ss [] t)
   and get_root_after_pratt t =
@@ -592,7 +602,8 @@ let scope_rule :
            ; m_lhs_arities = Hashtbl.create 7
            ; m_lhs_names   = Hashtbl.create 7
            ; m_lhs_size    = 0
-           ; m_lhs_in_env  = nl @ List.map fst pvs_rhs }
+           ; m_lhs_in_env  =
+               nl @ List.map fst pvs_rhs @ List.map fst pvs_when}
     in
     let lhs = scope ~find_sym 0 mode ss Env.empty p_lhs in
     match mode with
@@ -623,7 +634,28 @@ let scope_rule :
   let arity = List.length lhs in
   let f i = try Hashtbl.find names i with Not_found -> string_of_int i in
   let names = Array.init vars_nb f in
-  let r = {lhs; names; rhs; arity; arities; vars_nb; xvars_nb; rule_pos} in
+  let asPatt t = match unfold t with
+    | Patt (Some i, _, [||]) -> i
+    | _ -> fatal rule_pos "arguments should be patterns in condition [%a]."
+             term t in
+  let asSymb t =
+    match unfold t with
+    | Symb s -> s
+    | _ -> fatal rule_pos "symbol expected [%a]." term t in
+  let p_asPatt t = asPatt (scope ~find_sym 0 mode ss Env.empty t) in
+  let p_asSymb t = asSymb (scope ~find_sym 0 mode ss Env.empty t) in
+  let pw2rw t =
+    let t = scope ~find_sym 0 mode ss Env.empty t in
+    match get_args t with
+      Symb s, args ->  (s, List.map asPatt args)
+    | _ -> fatal rule_pos "function should be a global symbol in [%a]." term t
+  in
+  let r_when = match p_when with
+    | P_None -> R_None
+    | P_EQ (t1,t2) -> R_EQ (pw2rw t1, pw2rw t2)
+    | P_ST (o,t1,t2) -> R_ST (p_asSymb o, p_asPatt t1, p_asPatt t2) in
+  let r = {lhs; names; rhs; arity; arities; vars_nb; xvars_nb;
+           rule_pos; r_when} in
   (sym,r)
 
 (** [scope_pattern ss env t] turns a parser-level term [t] into an actual term
diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml
index be3357f14..9b7a4caeb 100644
--- a/src/parsing/syntax.ml
+++ b/src/parsing/syntax.ml
@@ -133,8 +133,13 @@ let rec pvars_lhs : p_term -> StrSet.t = fun {elt;pos} ->
   | P_Expl u
     -> pvars_lhs u
 
+type p_constraint =
+  P_EQ of p_term * p_term           (* t1 == t2 *)
+| P_ST of p_term * p_term * p_term  (* t2 <<[t1] t3 *)
+| P_None
+
 (** Parser-level rewriting rule representation. *)
-type p_rule_aux = p_term * p_term
+type p_rule_aux = p_term * p_term * p_constraint
 type p_rule = p_rule_aux loc
 
 (** Parser-level inductive type representation. *)
@@ -182,7 +187,8 @@ module P  = struct
   let abst_list : p_ident option list -> p_term -> p_term = fun idopts t ->
     List.fold_right abst idopts t
 
-  let rule : p_term -> p_term -> p_rule = fun l r -> Pos.none (l,r)
+  let rule : p_term -> p_term -> p_constraint -> p_rule =
+    fun l r w -> Pos.none (l,r,w)
 end
 
 (** Rewrite patterns as in Coq/SSReflect. See "A Small Scale
@@ -403,8 +409,21 @@ and eq_p_params : p_params eq = fun (i1,ao1,b1) (i2,ao2,b2) ->
   List.eq (Option.eq eq_p_ident) i1 i2
   && Option.eq eq_p_term ao1 ao2 && b1 = b2
 
-let eq_p_rule : p_rule eq = fun {elt=(l1,r1);_} {elt=(l2,r2);_} ->
-  eq_p_term l1 l2 && eq_p_term r1 r2
+let eq_p_constraint: p_constraint eq = fun c1 c2 ->
+  match c1,c2 with
+    P_EQ (t1,u1), P_EQ (t2,u2) -> eq_p_term t1 t2 && eq_p_term u1 u2
+  | P_ST (o1,t1,u1), P_ST (o2,t2,u2) ->
+      eq_p_term o1 o2 && eq_p_term t1 t2 && eq_p_term u1 u2
+  | P_None, P_None -> true
+  | _ -> false
+
+let pair_eq: 'a eq -> 'b eq -> ('a * 'b) eq = fun eq1 eq2 (x1,y1) (x2,y2) ->
+  eq1 x1 x2 && eq2 y1 y2
+
+let eq_p_rule : p_rule eq = fun {elt=(l1,r1,w1);_} {elt=(l2,r2,w2);_} ->
+  eq_p_term l1 l2
+  && eq_p_term r1 r2
+  && eq_p_constraint w1 w2
 
 let eq_p_inductive : p_inductive eq =
   let eq_cons (i1,t1) (i2,t2) = eq_p_ident i1 i2 && eq_p_term t1 t2 in
@@ -618,8 +637,15 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a =
 
   let fold_term : 'a -> p_term -> 'a = fold_term_vars StrSet.empty in
 
-  let fold_rule : 'a -> p_rule -> 'a = fun a {elt=(l,r);_} ->
-    fold_term (fold_term a l) r
+  let fold_constraint : 'a -> p_constraint -> 'a = fun a w ->
+    match w with
+    | P_EQ (t1,t2) -> fold_term (fold_term a t1) t2
+    | P_ST (o,t1,t2) -> fold_term (fold_term (fold_term a o) t1) t2
+    | P_None -> a
+  in
+
+  let fold_rule : 'a -> p_rule -> 'a = fun a {elt=(l,r,w);_} ->
+    fold_constraint (fold_term (fold_term a l) r) w
   in
 
   let fold_rwpatt_vars : StrSet.t -> 'a -> p_rwpatt -> 'a = fun vs a p ->
diff --git a/src/tool/lcr.ml b/src/tool/lcr.ml
index 42719d12b..ef2b81f35 100644
--- a/src/tool/lcr.ml
+++ b/src/tool/lcr.ml
@@ -55,7 +55,7 @@ let is_definable : sym -> bool = fun s ->
 (** [rule_of_def s d] creates the rule [s --> d]. *)
 let rule_of_def : sym -> term -> rule = fun s rhs ->
   {lhs=[]; names=[||]; rhs; arity=0; arities=[||]; vars_nb=0; xvars_nb=0;
-   rule_pos=s.sym_pos}
+   rule_pos=s.sym_pos; r_when = R_None}
 
 (** [replace t p u] replaces the subterm of [t] at position [p] by [u]. *)
 let replace : term -> subterm_pos -> term -> term = fun t p u ->
@@ -457,7 +457,7 @@ let typability_constraints : Pos.popt -> term -> subs option = fun pos t ->
     match get_args_len l with
     | Symb s, lhs, arity ->
       let r = {lhs; names=[||]; rhs; arity; arities=[||]; vars_nb=0;
-               xvars_nb=0; rule_pos=Some(new_rule_id())} in
+               xvars_nb=0; rule_pos=Some(new_rule_id()); r_when = R_None} in
       Some (s,r)
     | _ -> None
   in
diff --git a/src/tool/tree_graphviz.ml b/src/tool/tree_graphviz.ml
index 3097edf56..2780eb305 100644
--- a/src/tool/tree_graphviz.ml
+++ b/src/tool/tree_graphviz.ml
@@ -46,6 +46,11 @@ let tree_to_dot : Format.formatter -> _ dtree -> unit = fun ppf dtree ->
       | CondNL((i,vi), (j,vj)) ->
           out ppf "%d[%a] ≡ %d[%a]" i ar vi j ar vj
       | CondFV(i,vs) -> out ppf "%a ⊆ FV(%d)" ar vs i
+      | CondST(op,i,j) -> out ppf "%d «[%s] %d" (fst i) (snd op) (fst j)
+      | CondEQ(((_p1,s1),a1), ((_p2,s2),a2)) ->
+          out ppf "%s[%a] ≡ %s[%a]"
+            s1 (List.pp int ",") (List.map fst a1)
+            s2 (List.pp int ",") (List.map fst a2)
     in
     let node_count = ref 0 in
     (* [write_tree n u v] writes tree [v] obtained from tree number [n] with a
diff --git a/tests/OK/cond_rules.lp b/tests/OK/cond_rules.lp
new file mode 100644
index 000000000..0402de7e0
--- /dev/null
+++ b/tests/OK/cond_rules.lp
@@ -0,0 +1,20 @@
+symbol Prop: TYPE;
+symbol ∧: Prop → Prop → Prop;
+notation ∧ infix right 7;
+constant symbol ⊤ : Prop;
+constant symbol ⊥ : Prop;
+
+sequential symbol doubles_in_and : Prop → Prop;
+sequential symbol occurs_in_and : Prop → Prop → Prop;
+
+rule doubles_in_and ($p ∧ $q) when occurs_in_and $p $q ≡ ⊤ ↪ ⊤
+with doubles_in_and (_ ∧ $q) ↪ doubles_in_and $q
+with doubles_in_and _ ↪ ⊥;
+
+rule occurs_in_and $p $p ↪ ⊤
+with occurs_in_and $p ($p ∧ _) ↪ ⊤
+with occurs_in_and $p (_ ∧ $q) ↪ occurs_in_and $p $q
+with occurs_in_and _ _ ↪ ⊥;
+
+assert p q r ⊢ doubles_in_and (p ∧ q ∧ r) ≡ ⊥;
+assert p q r ⊢ doubles_in_and (p ∧ q ∧ p ∧ r) ≡ ⊤;
diff --git a/tests/OK/cond_rules_st.lp b/tests/OK/cond_rules_st.lp
new file mode 100644
index 000000000..9a8d98fcd
--- /dev/null
+++ b/tests/OK/cond_rules_st.lp
@@ -0,0 +1,15 @@
+symbol Prop: TYPE;
+symbol ∧: Prop → Prop → Prop;
+notation ∧ infix right 7;
+constant symbol ⊤ : Prop;
+constant symbol ⊥ : Prop;
+
+sequential symbol doubles_in_and : Prop → Prop;
+
+rule doubles_in_and ($p ∧ $q) when $p «[@∧] $q ↪ ⊤
+with doubles_in_and ($p ∧ $q) ↪ doubles_in_and $q
+with doubles_in_and $p ↪ ⊥;
+
+
+assert p q r ⊢ doubles_in_and (p ∧ q ∧ r) ≡ ⊥;
+assert p q r ⊢ doubles_in_and (q ∧ p ∧ r ∧ p) ≡ ⊤;
diff --git a/tests/export_dk.sh b/tests/export_dk.sh
index 741967625..d53991647 100755
--- a/tests/export_dk.sh
+++ b/tests/export_dk.sh
@@ -49,6 +49,8 @@ do
         Tactic|1374);;
         # use Tactic
         first_hyp|all_hyps);;
+        # use cond rules
+        cond_rules*);;
         # requires an excluded file
         assume|first_hyp);;
         # default case
diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh
index 860ea29cb..fd01bc2bf 100755
--- a/tests/export_raw_dk.sh
+++ b/tests/export_raw_dk.sh
@@ -58,6 +58,8 @@ do
         require_nondkmident);;
         # module alias
         alias);;
+        # conditional rules
+        cond_rules*);;
         # proofs
         why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit|change|assumption|focus|assume|first_hyp|all_hyps);;
         # "open"