Proving dependent equalities in Coq with SSReflect

Proving dependent equalities in Coq is boring, but quite frequently done.

Causation in modern philosophy of science

Our minds use the notions of cause and consequences all the time. It is, without a doubt, one of the fundamentals of human reasoning. However, when observed closely and formally, it becomes apparent that our concept is based rather on intuition and lacks strictness and connection to the real word. This post is intended as a quick introduction to causation from the philosophical point of view.

How to prove certain type inequalities in Coq

Sometimes you just want to prove that nasty ~ T = U for some types T and U. Well, while in general it is not decidable (nor provable), sometimes there is a relatively easy way to do it, when T and U are not both infinite. In other words, either T or U, or both of them should be finite.