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