ord_compl:

Add and prove {widen,narrow,lift,lower}_S_inj,
              filterP_ord_ind_l_in_0_equiv, filterP_ord_ind_r_in_max_equiv.
WIP: filterP_ord_ind_l_in_n0.

Finite_family:
Nope!