1 files changed, 6 insertions, 0 deletions
diff --git a/src/Misc.v b/src/Misc.v
index 2aa6b0e..889219e 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -1008,3 +1008,9 @@ Implicit Arguments forallb2 [A B].
    coq-load-path: ((rec "." "SMTCoq"))
    End: 
 *)
+
+Lemma neg_eq_true_eq_false b : b = false <-> b <> true.
+Proof. destruct b; intuition. Qed.
+
+Lemma is_true_iff e :  e = true <-> is_true e.
+Proof. now unfold is_true. Qed.