proposition: Lemma intro_state_correct_None : forall f st hf d (EQ : hf.(elt) = f) (WF : has_form (hconsmap st) hf) (WFST : wf_state st) (INTRO : intro_state st f hf = Success d), eval_state st -> eval_annot_state st -> eval_formula f.
proof: Proof. intros. generalize (intro_state_correct f st hf EQ WF WFST). rewrite INTRO. tauto. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause