for l1, l2 being Nat st goto l1 = goto l2 holds
l1 = l2