proposition: Lemma andb_permute : forall a b c, a && (b && c) = b && (a && c).
proof: Proof. intros; repeat rewrite andb_assoc; replace (a && b) with (b && a) by apply andb_comm; 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