[Hol-info] data-respecting relation

[Ramana K. <ram...@gm...>]

What is the usual name for this kind of relation?

Given an inductive data type like
foo = C1 of bool | C2 of foo list

I want to classify relations R:foo -> foo -> bool that satisfy:
1. equivalence R
2. EVERY2 R vs1 vs2 ==> R (C2 vs1) (C2 vs2)
3. R (C1 _) v ==> ?b. v = (C1 b) /\ R (C2 _) v ==> ?vs. v = (C2 vs)

Condition 1 alone is obviously an equivalence relation.
I think Conditions 1 + 2 give you a "congruence relation".
Any standard name or theory about 1 + 2 + 3?
Or maybe 3 should be included for congruences?

(Context: I'm trying to generalise a theorem that says some operation
preserves values up to a suitable equivalence of values, but equivalence is
subtle because my values include closures that contain code and other
(environment) values, and all I really care about in the end is that they
behave the same. In full generality this is a contextual equivalence
problem, which I don't want to solve; and indeed the approach above would
still require the code to be identical (since it's a different type). But
it might be useful to prove the theorem for a class of congruence
relations, rather than a specific one, and/or it might make the proof
slightly simpler...
And I could allow the code to vary by defining "congruence" for both the
value and code types together...)