A note on formal reasoning with extensible domains