Adding only tick variables as implicit binders

[aseemr]

//
// Pulse checker adds implicit binders for 'n1 and 'n2
//   at erased types
//
fn swap (r1 r2:ref U32.t)
  requires
      pts_to r1 'n1 **
      pts_to r2 'n2
  ensures
      pts_to r1 'n2 **
      pts_to r2 'n1



//
// Since p and n are non tick variables,
//   this gives an error "Identifiers (n, p) not found, consider adding them as binders"
//
[@@ expect_failure]
fn test_read (r:ref U32.t)
   requires pts_to r #p n
   returns x : U32.t
   ensures pts_to r #p x