I'm reading Wadler's paper called "How to make adhoc polymorphism less ad hoc". I'm trying to understand the given rules for function overload (over and inst) and I want to create a small example of a proof tree using them. All deductions rules are in Figure 9 and Figure 10.
I decided to proof the following expression/type: $(over\: eq:: Eq\: \alpha\: in\: inst\: eq :: Eq\:Int \:=\: eqInt\: in\: eq\:1\:2)::Bool$.
Some people gave me a tip: construct the tree in bottom-up.
I think I'm stuck. I have no idea how to go up in the tree. And I'm not sure if I can, at some point, discharge the assumption about $eqInt$.
I would like to know what I'm doing wrong and how to finish this proof.
EDIT: As said in the paper, $Eq\: \tau$ is a abbreviation for $\tau \rightarrow \tau \rightarrow Bool$.