proposition: Lemma check_annot_shorten_clause : forall hm l u wc d (WF : wf_units_lit u hm) (HCL : has_watched_clause hm wc) (HL : wf_pset hm (Annot.deps l)) (HA : wf_pset hm d), check_annot has_clause hm (shorten_clause l u d wc).
proof: Proof. unfold shorten_clause. intros. destruct_in_goal OPP. - apply check_annot_reduce; auto. inv HCL. inv H2;auto. inv HCL. inv H2;auto. apply wf_pset_union; auto. - destruct_in_goal OPP1. apply check_annot_reduce; auto. inv HCL. inv H2;auto. inv HCL. inv H2;auto. apply wf_pset_union; auto. apply check_annot_TRUE. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause