proposition: Lemma st_trans e1 e2 e3 : st_leq e1 e2 -> st_leq e2 e3 -> st_leq e1 e3.
proof: Proof. move: e1 e2 e3=>[p1 e1 S1 D1 F1][p2 e2 S2 D2 F2][p3 e3 S3 D3 F3]. case=>/= E1 R1 [/= E2 R2]; rewrite /st_leq /=. have E3 := poset_trans E2 E1; exists E3=>i V P y m. set P' := E2 i P. move: (R1 i V P' y m)=>{}R1; move: (R2 i V P y m)=>{}R2. move=>H1; apply/R2/R1. by rewrite (pf_irr (E1 i P') (E3 i P)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)