proposition: Lemma intro_state_mono : forall st st' f hf g', intro_state st f hf = Progress (st', g') -> hmap_order (hconsmap st) (hconsmap st').
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); try congruence. simpl. destruct o; simpl; try congruence. specialize (hconsmap_augment_cnf false (NEG h) st0). unfold hconsmap_progress. destruct (augment_cnf false (NEG h) st0); try congruence. inv H. simpl. intros. intuition congruence. intuition congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause