pub fn data_refinement_ty() -> Expr
DataRefinement: a concrete implementation refines an abstract spec. Type: AbstractSpec → ConcreteImpl → Prop