Function prop_binding_generable 

pub fn prop_binding_generable(
    ty: TyId,
    types: &HashMap<String, Arc<TypeDecl>>,
    depth: u32,
    tys: &Arc<Types>,
) -> bool

Whether a for all x: T binding’s type is refinement-generable: refined types must not carry a Matches predicate (no refinement-driven generator), and sums/records must have every component recursively generable within the depth cap. Mirrors the checker’s can_mock_bare.