merged

added SMT certificates

use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)

fixed eta-expansion: use correct order to apply new bound variables

check if negating the goal is possible (avoids CTERM exception for Pure propositions)

unfold and eta-contract let expressions before lambda-lifting to avoid bad terms

corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables