proposition: Lemma st_asym e1 e2 : st_leq e1 e2 -> st_leq e2 e1 -> e1 = e2.
proof: Proof. move: e1 e2=>[p1 e1 S1 D1 F1][p2 e2 S2 D2 F2]; rewrite /st_leq /=. case=>E1 R1 [E2 R2]. move: (poset_asym E1 E2)=>?; subst p2. have : e1 = e2. - apply: fext=>i; apply: fext=>Vi; apply: fext=>Pi; apply: fext=>y; apply: fext=>m. move: (R2 i Vi Pi y m)=>{}R2; move: (R1 i Vi Pi y m)=>{}R1. apply: pext; split. - by move=>H1; apply: R1; rewrite (pf_irr (E1 i Pi) Pi). by move=>H2; apply: R2; rewrite (pf_irr (E2 i Pi) Pi). move=>?; subst e2. by congr Prog; apply: pf_irr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)