Description: Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf . (Contributed by Raph Levien, 10-Apr-2004) (Proof shortened by Wolf Lammen, 25-Jan-2025)