diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index f2015ffb1c55f2c4629c1ec79ea21c667eb88f0a..b759702b9a3763bd3188d13dfe6142bd874cdf0f 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -235,6 +235,7 @@ struct
     match t1, t2 with
     | None, None -> true
     | None, Some _ | Some _ , None -> false
+    | Some (Bool|Prop) , Some(Bool|Prop) -> true
     | Some t1, Some t2 -> Tau.equal t1 t2
 
   let sort x = x.sort