proposition: Lemma order_dom_trans : forall {A B C: Type} (m1: IntMap.ptrie A) (m2: IntMap.ptrie B) (m3: IntMap.ptrie C), order_dom m1 m2 -> order_dom m2 m3 -> order_dom m1 m3.
proof: Proof. unfold order_dom. intros. apply H in H1. apply H0 in H1. auto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause