Proved cadd_cmult_distrib.

Now proof of Ord_jump_cardinal uses ordertype_pred_unfold; proof of sum_0_eqpoll uses bij_0_sum; proof of sum_0_eqpoll uses sum_prod_distrib_bij; proof of sum_assoc_eqpoll uses sum_assoc_bij; proof of prod_assoc_eqpoll uses prod_assoc_bij. Proved well_ord_cadd_cmult_distrib.

Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong uses lemma sum_bij; proof of prod_eqpoll_cong uses lemma prod_bij.

pretty_gram: now sorts productions;

removed print_sign, print_axioms;

slightly changed OFCLASS syntax;