proposition: Theorem andb_commutative : forall b c, andb b c = andb c b.
proof: Proof. intros b c. destruct b. - destruct c. + reflexivity. + reflexivity. - destruct c. + reflexivity. + reflexivity. Qed.
imports: Coq(Arith List) LF(IndProp) Coq(Lia)