proposition: Lemma singleP i : i \In defed P -> this i <== defed P.
proof: Proof. by move=>[pf1 pf2] h <-; split. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) LemmaOverloading(prelude heaps rels hprop domains)