proposition: Lemma hconsmap_unit_propagation : forall n g st, hconsmap_progress (unit_propagation n g) st.
proof: Proof. repeat intro. revert st H. induction n. - simpl. repeat intro. tauto. - intros. rewrite unit_propagation_rew in H. rewrite unit_propagation_rew. destruct (extract_unit st) eqn:EQ. + destruct p. apply hconsmap_extract_unit in EQ. destruct (success g (units s) t0). * simpl. congruence. * generalize (hconsmap_insert_literal t0 s). set (sti := (insert_literal t0 s)) in * ; clearbody sti. simpl in *. intros. set (lc := (WMap.find_clauses (Annot.elt t0) (clauses sti))) in *. generalize (hconsmap_shorten_clauses t0 lc sti). unfold hconsmap_progress. set (sts := shorten_clauses t0 lc sti) in *. clearbody sts. destruct sts ; simpl in * ; intuition try congruence. rewrite IHn;auto. congruence. + reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause