proposition: Lemma orb_is_associative : ∏ b1 b2 b3 : bool, orb (orb b1 b2) b3 = orb b1 (orb b2 b3).
proof: Proof. intros; induction b1; induction b2; induction b3; reflexivity. Qed.
imports: UniMath.Foundations.Init UniMath.Foundations.Sets