proposition: Lemma prog_sup_frame u : frameable (prog_sup u).
proof: Proof. move=>i j Pi Vij Pij y m [e][He]Pe. have Pi' := Pi e He; have Pij' := Pij e He. move: Pe; rewrite (pf_irr (pre_sup_leq He Pij) Pij'). case/(fr_st Pi' Vij Pij')=>h [{m}-> Vhj Ph]. exists h; split=>//; exists e, He. by rewrite (pf_irr (pre_sup_leq He Pi) Pi'). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)