proposition: Lemma has_form_find : forall m f, has_form m f -> IntMap.get' f.(id) m <> None.
proof: Proof. intros. inv H; simpl; congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause