proposition: Lemma umfiltT0 V (k1 k2 : stamp) (f : natmap V) : k1 \in dom f -> k2 \in dom f -> um_filterk (ltn^~ k1) f = Unit -> um_filterk (ltn^~ k2) f = Unit -> k1 = k2.
proof: Proof. by move=>D1 D2 U1 U2; apply: umfiltT D1 D2 _ _; rewrite ?U1 ?U2 dom0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)