Replaced instance declarations for sets by instance declarations for bool. Together with the instance declarations for fun from Ffun, this subsumes the old instance declarations for sets.

Adm now imports Ffun rather than Cont, because SetPcpo, which imports Adm, needs functions (since sets are now just functions).

Lookup and union operations on terms are now modulo eta conversion.

Terms returned by decomp are now eta-contracted.

Added function for computing instantiation for the subst rule, which is used in vars_gen_hyp_subst_tac and blast_hyp_subst_tac to avoid problems with HO unification.

eq_assumption now uses aeconv instead of aconv.

- Removed function eta_contract_atom, which did not quite work - Corrected and simplified function aeconv

Replaced Pattern.eta_contract_atom by Envir.eta_contract.

Removed instantiation for set.

Explicitely applied ext in proof of tnd.

Deleted subset_antisym in a few proofs, because it is accidentally applied to predicates as well.

- Tuned imports - Replaced blast by simp in proof of Stable_final_E_NOT_empty, since blast looped because of the new encoding of sets.

Manually applied subset_antisym in proof of Compl_fixedpoint, because it is accidentally applied to predicates as well.

Replaced blast by fast in proof of INT_Un_Compl_subset, since blast looped because of the new encoding of sets.