proposition: Theorem anti_literals_in: forall p z1 z2, In z2 ref_list -> z2 <> z1 -> In (L p z2) (anti_literals (L p z1)).
proof: Proof. intros (x1, y1) z1 z2 H H1. unfold anti_literals. repeat match goal with |- In ?X (clause_merge ?Y ?Z) => case (clause_merge_in X Y Z); intros _ tmp; apply tmp; clear tmp; right end. match goal with |- In ?X (lit_rm ?Y ?Z) => case (lit_rm_in X Y Z); try (intros _ tmp; apply tmp; clear tmp) end. red; apply olist_one. apply gen_cell_ordered. split. simpl; intros [H2 | H2]; case H1; try injection H2; auto. case H2. case (gen_cell_correct (L (Pos x1 y1) z2) x1 y1); auto; intros _ tmp; apply tmp; clear tmp. exists z2; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia