proposition: Lemma subdom_trans h2 h1 h3 : subdom h1 h2 -> subdom h2 h3 -> subdom h1 h3.
proof: Proof. move=>H1 H2; move: (subdom_def H1) (subdom_def H2). case/andP=>D1 _; case/andP=>_ D2. case E: (empb h1). - by move/empP: E =>->; rewrite subdom_emp. apply/subdomP=>[//||x in1]; first by apply negbT. by apply: (subdomQ H2) (subdomQ H1 in1). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep