proposition: Lemma andb_implication_preserve : forall a b, (a = true -> b = true) -> a = b && a.
proof: Proof. intros; destruct a; destruct b; symmetry; auto. 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