compact_relation bs as_ps: Produce a relation of the form: R as := ∃ bs, Λ_i a_i = p_i[bs] This relation is user visible, so we compact it by removing each b_j where a p_i = b_j, and hence a_i = b_j. We need to take care when there are p_i and p_j with p_i = p_j = b_k.

TODO: this is copied from Lean's coinductive_predicates.lean, export it there.

mk_iff_of_inductive_prop i r makes a iff rule for the inductively defined proposition i. The new rule r has the shape ∀ps is, i as ↔ ⋁_j, ∃cs, is = cs, where ps are the type parameters, is are the indices, j ranges over all possible constructors, the cs are the parameters for each constructors, the equalities is = cs are the instantiations for each constructor for each of the indices to the inductive type i.

In each case, we remove constructor parameters (i.e. cs) when the corresponding equality would be just c = i for some index i.

For example: mk_iff_of_inductive_prop on list.chain produces:

∀{α : Type*} (R : α → α → Prop) (a : α) (l : list α), chain R a l ↔ l = [] ∨ ∃{b : α} {l' : list α}, R a b ∧ chain R b l ∧ l = b :: l'