New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.

use_thys ["Paper"];