Lemma orb_is_commutative : ∏ b1 b2 : bool, orb b1 b2 = orb b2 b1. Proof. intros; induction b1; induction b2; reflexivity. Qed.
Require Import UniMath.Foundations.Init. Require Import UniMath.Foundations.Sets.