proposition: Lemma wf_shorten_clause : forall m l u cl an (WFL : check_annot has_literal m l) (WFU : wf_units_lit u m) (WFA : wf_pset m an) (WFC : has_watched_clause m cl), check_annot has_clause m (shorten_clause l u an cl).
proof: Proof. intros. unfold shorten_clause. destruct_in_goal OPP. - split. apply wf_pset_reduce; auto. apply wf_pset_union;auto. destruct WFL;auto. unfold has_watched_clause in WFC. do 2 rewrite Forall_rew in WFC. apply has_clause_reduce; auto; tauto. - destruct_in_goal OPP1. split. apply wf_pset_reduce; auto. apply wf_pset_union;auto. destruct WFL;auto. unfold has_watched_clause in WFC. do 2 rewrite Forall_rew in WFC. apply has_clause_reduce; auto; tauto. 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