d2 = [x:nat](d1 1!x)
     : (x,x0:nat)x0=x ->x0=x

Positions [1; 2] are implicit
Argument scopes are [nat_scope nat_scope _]