reverted 3e1d230f1c00 -- pervasiveness is useful, cf. Coinductive_Nat in the AFP

simplified code

fourth attempt at generalizing N2M types (to leverage caching)

tuning

int and nat are conditionally_complete_lattices

be more open-minded and allow needless mutual recursion for 'prim(co)rec', since we allow it for '(co)datatype' -- eventual warnings (or errors) should be centralized in 'fp_bnf'

removed dead code

update docs

take out possibility of moving corecursive calls past constructors -- this doesn't work in the general case

took out loopy code