Depends what you want to do. If you are interested in program verification, then not all that much, because everything is about automation. Coq/Agda have a sma

Depends what you want to do. If you are interested in program verification, then not all that much, because everything is about automation. Coq/Agda have a small edge if you want to prove something about Lambda calculus since Coq/Agda are themselves Lambda calculi, and not surprisingly most Coq/Agda work is about Lambda calculus ... The HOL school has probably a small edge in other areas. In practise the underlying approach (LCF vs Curry-Howard and dependent types vs HOL) makes much less of a difference than automation and availablility of proof libraries.