feat(style.md): first cut at style guidelines
feat(list.lean): start on list library
feat(equality_test.lean): experiments with equality axioms

This reduces most of the current axioms for equality and heterogeneous equality to the basic rules for Id as an inductive type, plus Pi injectivity. There are universe problems that should go away in Lean 0.2.