Function commit_binding_ty 

pub fn commit_binding_ty() -> Expr

CommitBinding : CommitmentScheme → Prop

Binding: it is computationally infeasible to open a commitment to two different values (m, r) and (m', r') with m ≠ m'.