pub fn refinement_mapping_ty() -> Expr
RefinementMapping: a coupling function between abstract and concrete states. Type: {A C : Type} → (C → A) → Prop