diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-06-30 16:02:36 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-06-30 16:02:36 +0200 |
| commit | dbbdbff6f25c9f4cc9a7203d7e038bbbb549f7b1 (patch) | |
| tree | 9f1338e5ebb62643a469b2759c25d657d8692f7c /src/State.v | |
| parent | dc786cea07fc7c2f9323d57a60d4731ebe97a577 (diff) | |
| download | smtcoq-dbbdbff6f25c9f4cc9a7203d7e038bbbb549f7b1.tar.gz smtcoq-dbbdbff6f25c9f4cc9a7203d7e038bbbb549f7b1.zip | |
Remove axiom
Diffstat (limited to 'src/State.v')
| -rw-r--r-- | src/State.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/State.v b/src/State.v index a3af611..4b0db6d 100644 --- a/src/State.v +++ b/src/State.v @@ -424,6 +424,13 @@ Module C. unfold valid, interp;destruct c;simpl; auto;discriminate. Qed. + Lemma Cinterp_neg rho cl : + interp rho (List.map Lit.neg cl) = negb (List.forallb (Lit.interp rho) cl). + Proof. + induction cl as [ |l cl IHcl]; auto. + simpl. now rewrite negb_andb, IHcl, Lit.interp_neg. + Qed. + End C. |