take {} ; :: thesis: {} is f -unambiguous
thus {} is f -unambiguous by Lm14; :: thesis: verum