proposition: Lemma to_bits_of_bits (b : _) : to_bits (of_bits b) = b.
proof: Proof. repeat match goal with | p : prod _ _ |- _ => destruct p | b : bool |- _ => destruct b end; exact eq_refl. Qed.
imports: Coq.Init.Ltac Coq.Init.Datatypes Coq.Init.Logic Coq.Init.Specif