diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-28 12:39:33 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-28 12:39:33 +0000 |
| commit | 82e4ba006786491640597ea07016708105860a52 (patch) | |
| tree | 3550b6dada3d99dbce52682f6411728edd8602f1 /theories/Bool | |
| parent | c2d532e58bff5ae38c613c695b674bb667c86dfe (diff) | |
Ajout andb_true_eq pour PolyList.list_beq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2497 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Bool')
| -rwxr-xr-x | theories/Bool/Bool.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 6b5a1f863..f8b50e6c2 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -322,6 +322,11 @@ Proof. Save. Hints Resolve andb_prop : bool v62. +Definition andb_true_eq : (a,b:bool) true = (andb a b) -> true = a /\ true = b. +Proof. + Destruct a; Destruct b; Clear a b; Auto. +Defined. + Lemma andb_prop2 : (a,b:bool)(Is_true (andb a b)) -> (Is_true a)/\(Is_true b). Proof. |