proposition: Lemma insert_normalised_clause_mono : forall i cl st, hconsmap_progress (insert_normalised_clause i cl) st.
proof: Proof. unfold insert_normalised_clause. repeat intro. destruct (Annot.elt cl) ; simpl ; auto with wf. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause