cohomology: new suspension axiom for 0th cohomology
move def of iterated susp to lib.types; define S_n