sftypes/software-foundations — pull request #1 by winitzki (2014-04-17 19:07:59+00:00)
Title: adding my solutions written up so far

Basics: complete.
Induction: all except the hardest exercise:
`Theorem bin_of_nat_normalized_sound: forall (b:bin), bin_of_nat(nat_of_bin b) = bin_normalize b.`