What were the things that were confusing? I tried it out and found it much more intuitive than Coq (especially in the proofs). The keywords made sense, and so did the error messages. That said, I come from a more math oriented background, and I've played typed around with this sort of thing for a while now. So yeah, I'm honestly interested in hearing your perspective!