Right EvTerm for `a ~ b`

If I have two types data L and data H, and I want to "pretend" that I've solved (H ~ L or L ~ H) in a type checker plugin, what's the right EvTerm to use? The two types don't have any constructors, so they should be coercible. I've been using evCoercion $ mkReflCo Phantom anyTy and it doesn't panic... but I don't know if that's the right choice.