1	import Base
2	import ./type.bend as R
3	import ./ops.bend as O
4	
5	# LAW: a tree's first key is its own
6	law first_key_is_own:
7	  for -N: Data
8	  for +r: R.Rose<N>
9	  {O.first(O.keys(N, [r])) == O.key(N, r) : String}