> Coq is ridiculously powerful, but hardly beautiful. I agree, hence my qualification that it relies on an imperative layer (Ltac) to do anything useful, like

> Coq is ridiculously powerful, but hardly beautiful. I agree, hence my qualification that it relies on an imperative layer (Ltac) to do anything useful, like dependent pattern-matching. I've edited my potentially ambiguous phrasing.