The Metamath database contains proofs

Some of its theorems do not correspond to rules that can be applied subsequently
Does not pattern match subterms ; just replaces variables
Should show us the distance matrix (by proof steps) between different statements
[ Hand-woven fabric .... ]
[[[[ Want to show each step, not just overall dependency ]]]]]