proposition: Lemma hconsmap_intro_state : forall st f hf, ~ is_fail (intro_state st f hf) -> match intro_state st f hf with | Fail _ => False | Progress (st',_) => hconsmap st' = hconsmap st | Success (h,_) => h = hconsmap st end.
proof: Proof. unfold intro_state. intros. destruct (intro_impl nil f hf). generalize (hconsmap_cnf_hyps o l st). unfold hconsmap_progress. destruct (cnf_hyps (is_classic o) l st) eqn:EQ; simpl in *. - tauto. - destruct r ; auto. - destruct o ; auto. intros. generalize (hconsmap_augment_cnf false (NEG h) st0). unfold hconsmap_progress. destruct ((augment_cnf false (NEG h) st0)) ; simpl in *; try intuition congruence. + destruct r. intuition congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause