proposition: Lemma umfiltT V (k1 k2 : stamp) (f : natmap V) : k1 \in dom f -> k2 \in dom f -> k1 \notin dom (um_filterk (ltn^~ k2) f) -> k2 \notin dom (um_filterk (ltn^~ k1) f) -> k1 = k2.
proof: Proof. case/In_domX=>v1 D1 /In_domX [v2 D2] S1 S2. case: (ltngtP k1 k2)=>// N. - by move/(In_umfiltk (ltn^~ k2))/(_ N)/In_dom: D1; rewrite (negbTE S1). by move/(In_umfiltk (ltn^~ k1))/(_ N)/In_dom: D2; rewrite (negbTE S2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)