diff options
| author | Cyril Cohen | 2020-09-28 21:07:29 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-11-01 13:59:41 +0100 |
| commit | 21897f9663ac06a3cd9517f07b7e574335773cf8 (patch) | |
| tree | 0b410aa972f5cbfc7be35e6ab85727d72328b4db | |
| parent | f0dd790c5b142ac3afa36584551c1dd243b219ee (diff) | |
minimizing variables
Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
| -rw-r--r-- | mathcomp/ssreflect/ssrbool.v | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v index 0bc3f9a..48f0262 100644 --- a/mathcomp/ssreflect/ssrbool.v +++ b/mathcomp/ssreflect/ssrbool.v @@ -108,11 +108,8 @@ Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). Variables T1 T2 T3 : predArgType. -Variables (D1 D1' : {pred T1}) (D2 : {pred T2}) (D3 : {pred T3}). -Variables (d1 d1' : mem_pred T1) (d2 d2' : mem_pred T2) (d3 d3' : mem_pred T3). -Variables (f f' : T1 -> T2) (g : T2 -> T1) (h : T3). -Variables (P1 : T1 -> Prop) (P2 : T1 -> T2 -> Prop). -Variable P3 : T1 -> T2 -> T3 -> Prop. +Variables (D1 : {pred T1}) (D2 : {pred T2}). +Variables (f : T1 -> T2) (h : T3). Variable Q1 : (T1 -> T2) -> T1 -> Prop. Variable Q1l : (T1 -> T2) -> T3 -> T1 -> Prop. Variable Q2 : (T1 -> T2) -> T1 -> T1 -> Prop. @@ -352,4 +349,3 @@ Proof. by case: b => // /(_ isT). Qed. Lemma contra_notF P b : (b -> P) -> ~ P -> b = false. Proof. by case: b => // /(_ isT). Qed. End Contra. - |