proposition: Lemma unit_propagation_not_stuck : forall n g st, unit_propagation n g st = Fail Stuck -> False.
proof: Proof. induction n. - simpl. discriminate. - simpl. intros. destruct (extract_unit st). destruct p. destruct (success g (units s) t0). congruence. destruct (shorten_clauses t0 (WMap.find_clauses (Annot.elt t0) (clauses s)) (insert_literal t0 s) ) eqn:E; try congruence. inv H. apply shorten_clauses_not_stuck in E; auto. congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause