proposition: Lemma andb_orb_distrib_r_assoc : forall b1 b2 b3 b4 : bool, ((b1 && (b2 || b3)) || b4)%bool = (b1 && b2 || ((b1 && b3) || b4))%bool.
proof: Proof. repeat intros []; 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