proposition: Lemma prover_arrows_rew : forall (g : option HFormula) (st: state) (l : list literal), prover_arrows l st g = match l with | nil => Fail Stuck | e::l => let f := form_of_literal e in match prover_intro (remove_arrow e st) (Some f) with | Success (m,prf,d) => let st'' := insert_unit (annot_lit f) st in match augment_clauses prf (set_hmap m st'')with | Success (h,d) => Success (h,prf,d) | Progress st'' => ProverT st'' g | Fail f => Fail f end | Fail (OutOfFuel|InternalError) as e => e | Fail (HasModel | Stuck) | Progress _ => prover_arrows l st g end end.
proof: Proof. destruct l; reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause