Change order of some conj and disj.
Rename insertF_inj_l <-> insertF_inj_r, insertF_nextF_compat_l <-> insertF_nextF_compat_r, insert2F_inj_l -> insert2F_inj_r, insert2F_inj_r{0,1} -> insert2F_inj_l{0,1}, insert2F_nextF_compat_l -> insert2F_nextF_compat_r, insert2F_nextF_compat_r{0,1} -> insert2F_nextF_compat_l{0,1}, replaceF_reg_l <-> replaceF_reg_r, replaceF_neqxF_compat_l <-> replaceF_neqxF_compat_r, replace2F_reg_l -> replace2F_reg_r, replace2F_reg_r{0,1} -> replace2F_reg_l{0,1}, insertT{r,c,}_inj_l <-> insertT{r,c,}_inj_r, insertT{r,c,}_nextT_compat_l <-> insertT{r,c,}_nextT_compat_r, replaceT{r,c,}_reg_l <-> replaceT{r,c,}_reg_r, replaceT{r,c,}_neqxT{r,c,}_compat_l <-> replaceT{r,c,}_neqxT{r,c,}_compat_r, {insertF,replaceF}_zero_reg_l <-> {insertF,replaceF}_zero_reg_r, {insert2F,replace2F}_zero_reg_l -> {insert2F,replace2F}_zero_reg_r, {insert2F,replace2F}_zero_reg_r{0,1} -> {insert2F,replace2F}_zero_reg_l{0,1}, {insertT,replaceT}{r,c,}_zero_reg_l <-> {insertT,replaceT}{r,c,}_zero_reg_r,
Showing
- Algebra/Monoid/Monoid_FF.v 62 additions, 62 deletionsAlgebra/Monoid/Monoid_FF.v
- Algebra/Monoid/Monoid_FT.v 29 additions, 29 deletionsAlgebra/Monoid/Monoid_FT.v
- Subsets/Finite_family.v 88 additions, 88 deletionsSubsets/Finite_family.v
- Subsets/Finite_table.v 72 additions, 72 deletionsSubsets/Finite_table.v
Loading
Please register or sign in to comment