Finished proofs for W types, modulo univ inconsistencies.