proposition: Lemma le_add : forall E x T, find x E = None -> le E (add x T E).
proof: Proof. intros E x T hx y U' hy. rewrite add_mapsto_iff. right. intuition. rewrite H in hx. rewrite find_mapsto_iff, hx in hy. discr. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)