proposition: Lemma funeq_irreflexive r t (H: funeq r) (IRR: irreflexive (restr_eq_rel f t ⨾ r)) : irreflexive (t ⨾ r).
proof: Proof. unfold funeq, irreflexive, seq, restr_eq_rel in *. ins; desf; eauto 8 using eq_sym. Qed.
imports: HahnBase HahnRelationsBasic Setoid