fill in firstn/splitn and inversion proofs
fill in BLxor-preserves-length proofs
fill in two of the byte/bit proofs; stuck on the last two (inductive -> computational)