diff --git a/FiniteSets/disjunction.v b/FiniteSets/disjunction.v index fe8c1dd..f279413 100644 --- a/FiniteSets/disjunction.v +++ b/FiniteSets/disjunction.v @@ -176,10 +176,10 @@ Section hPropLattice. associative_max := _ ; idempotent_min := _ ; idempotent_max := _ ; - neutralL_min := _ ; - neutralR_min := _ ; + neutralL_max := _ ; + neutralR_max := _ ; absorption_min_max := _ ; absorption_max_min := _ }. -End hPropLattice. \ No newline at end of file +End hPropLattice. diff --git a/FiniteSets/fsets/properties_decidable.v b/FiniteSets/fsets/properties_decidable.v index 3080817..9cf3ac3 100644 --- a/FiniteSets/fsets/properties_decidable.v +++ b/FiniteSets/fsets/properties_decidable.v @@ -208,8 +208,8 @@ Section SetLattice. associative_max := _ ; idempotent_min := _ ; idempotent_max := _ ; - neutralL_min := _ ; - neutralR_min := _ ; + neutralL_max := _ ; + neutralR_max := _ ; absorption_min_max := _ ; absorption_max_min := _ }.