begin
 down x1 . [][]<->x1;  { transitive }
 down x1 . [][]-x1;    { asymmetric }
 down x1 . <>x1        { reflexive  }
end