proposition: Lemma prog_sup_dstrict u : def_strict (prog_sup u).
proof: Proof. by move=>i P V y; case; case=>p e S D F [H1] /D. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)