proposition: Lemma wf_units_weaken : forall (u: IntMap.ptrie (Annot.t bool)) m, wf_units_lit u m -> wf_units_def u m.
proof: Proof. unfold wf_units_def, wf_units_lit. intros. destruct (IntMap.get' i u) eqn:EQ ; try congruence. apply H in EQ. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause