Function commitment_binding_ty 

pub fn commitment_binding_ty() -> Expr

CommitmentBinding : CommitmentScheme → Prop

Binding property: it is computationally infeasible to open a commitment to two different messages m ≠ m’, i.e., find (m, r), (m’, r’) such that Com(m, r) = Com(m’, r’).