Lambda the Ultimate

I want to produce traces of the type derivations for compositional type inference to help debugging programs. Currently the reports look like this:

var ---------------------------------------
x : {x : a} |- a

var ---------------------------------------
y : {y : a} |- a

x : {x : a} |- a
y : {y : a} |- a
app ---------------------------------------
(x y) : {x : (a -> b), y : a} |- b

var ---------------------------------------
z : {z : a} |- a

(x y) : {x : (a -> b), y : a} |- b
z : {z : a} |- a
app ---------------------------------------
((x y) z) : {x : (a -> (b -> c)), y : a, z : b} |- c

However repeating the typings in each derivation seems a bit of a waste of space. I am thinking I can just reference which rule is used and number the statements, a bit like a theorem proof. Something like:

1) var |= x : {x : a} |- a
2) var |= y : {y : a} |- a
3) app (1) (2) |= (x y) : {x : (a -> b), y : a} |- b
4) var |= z : {z : a} |- a
5) app (3) (4) |= ((x y) z) : {x : (a -> (b -> c)), y : a, z : b} |- c

Does this seem a reasonable notation? it the use of the double-turnstile "|=" a misuse of notation? Is there a better way to write this?