TODO:

Basics.v

induction.v
    Theorem norm_bin_nat_bin: forall b : bin, normalize b = nat_to_bin (bin_to_nat b).

Lists.v 
    How _many_ elements does the type [baz] have?

Poly.v
    Theorem nth_of_length_n: forall X l n, length l = n -> @nth_error X l n = None.
    Definition exp (n m : cnat) : cnat

Tactics.v

Logic.v
    (all from
    Theorem contrapositive : forall (P Q : Prop), (P -> Q) -> (~Q -> ~P).
    
IndProp.v
    total_relation not sure
    empty_relation not sure
    (all from
    Theorem le_plus_l : forall a b, a <= a + b.

ProofObjects.v

IndPrinciples.v