Putting aside the Claudisms.

You only compare to tactic heavy languages, which is what you don't like about them. Try looking at Agda, Idris, Mikan,... They work with pattern matching not just for definitions but for proofs as well, so the derivation is laid bear.

Not saying your niche doesn't have value, but you can get interesting ideas from there.