Resolution rule:
A v B
~B v C
---------
A v C

As an Agda theorem:
f : ((A v B) ^ (~B v C)) -> (A v C)
f (left a , left ~b) = left a
f (left a, right c) = left a	# could also use right c
f (right b, left ~b) = ???		# need principle of explosion
f (right b, right c) = right c