proposition: Lemma fold_left_andb_andbr ls : forall b, List.fold_left andbr ls b = List.fold_left andb ls b.
proof: Proof. induction ls; simpl; trivial. intro; rewrite IHls, andbr_andb. reflexivity. Qed.
imports: Coq.Strings.String Coq.Strings.Ascii Coq.Arith.Arith Coq.ZArith.BinInt Coq.NArith.BinNat Coq.Bool.Bool Coq.Classes.Morphisms Fiat.Common.Coq__8_4__8_5__Compat