Added unfolding lemmas to basic_facts/ideal Fixed proofs depending on the previous definition using unfolding lemmas
The changes follow the discussion in Paris. @bbb @sbozhko @sophie could you have a look at the changes and tell me if everything looks ok?