∀y,x,f:Top. (int_formula_prop(f;x "=>" y) ~ int_formula_prop(f;x)
int_formula_prop(f;y))
{ (UnivCD THENA Auto) }
1. y : Top@i
2. x : Top@i
3. f : Top@i
⊢ int_formula_prop(f;x "=>" y) ~ int_formula_prop(f;x)
int_formula_prop(f;y)