Theorem btw_rfl_left

Modification history