Description: Membership in a class abstraction, using implicit substitution. Deduction version of elab . (Contributed by Gino Giotto, 12-Oct-2024)