clarified signature: fewer tuples;

clarified signature: more explicit get_proofs_level with bounds check;

merged

misc tuning and clarification: more standard Same.commit discipline;

tuned;

tuned names;

more operations; more accurate treatment of beta contraction in norm_term/norm_proof, following Envir.norm_term;

minor performance tuning: more careful treatment of empty environment;

clarified signature;

more zproofs;