Show HN: I wrote a toy proof assistent

It is an implementation of the Calculus of Constructions with a small set of axioms.