proposition: Lemma bound (p : ideald P) i : i \In id_val p -> i \In defed P.
proof: Proof. by case: p=>p H; case/H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)