proposition: Lemma fsupp_immediate_pred A (R: relation A) (FS: fsupp R) (IRR: irreflexive R) (TRANS: transitive R) x (NMIN: ~ min_elt R x): exists x', immediate R x' x.
proof: Proof. clarify_not. apply fsupp_imm_t, ct_end in NMIN; eauto. destruct NMIN; desf; eauto. Qed.
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted