fun c => (if c then
	forall n m:nat, Universe n -> Universe m -> Universe (max n m)
else
	forall n, Universe n -> Universe n).