Thm* assert_of_bimplies

Thm* assert_functionality_wrt_bimplies

Thm* bimplies_transitivity

Thm* bimplies_weakening

Thm* comb_for_bimplies_wf