∀x,f:Top.  (int_term_value(f;vx) ~ f x)
{ (UnivCD THENA Auto) }
1. x : Top@i
2. f : Top@i
⊢ int_term_value(f;vx) ~ f x