proposition: Lemma fsupp_seq_eqv_r r d (FS: fsupp r) : fsupp (r ⨾ ⦗d⦘).
proof: Proof. unfold fsupp, seq, eqv_rel; desf; ins; desf. specialize (FS y); desf; exists findom; ins; desf; eauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom