reduce the strip_labels theorems to two cheats

the sufficient lemmas are:

!bs. strip_labels (strip_labels bs) = strip_labels bs

and

!bs1 bs2. bc_next (strip_labels bs1) bs2 ==> ?bs3. bc_next bs1 bs3