Commit 2022-10-03 17:40 5ca6e9d2

feat(logic/relation): characterization of the accessible predicate in terms of well_founded_on (#16720)

• Show that acc r a (read: a is accessible under the relation r) if and only if r is well-founded on the subset of elements below a (transitively) under r, including (refl_trans_gen) or excluding (trans_gen) a. Stated as a list.tfae.
• Move relation.fibration (used by the proof) to logic/relation to avoid importing logic/hydra. Add lemma acc_trans_gen_iff used in the proof.