A few more proofs from Induction.v.