proposition: Lemma infinitary_op_to_binop {X : hSet} (op : ∏ I : UU, (I -> X) -> X) : binop X.
proof: Proof. intros x y; exact (op _ (bool_rect (fun _ => X) x y)). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions