failed attempt to prove that |- always has a set of hyps

because it doesn't: the instantiation rules might leave you with a list
of hyps that includes duplicates (up to aconv). e.g. instantiate a ->
num in [P a; P num] |- Q, and you get [P num; P num] |- Q.
type_ok_Fun, SYM_rule, and truth_thm

but fail to prove useful things about assumption manipulation