fix the reflexivity prover
made divide_pos_pos a simp rule
merged
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced