proposition: Theorem lit_insert_in: forall l1 l2 c, In l1 (lit_insert l2 c) <-> l1 = l2 \/ In l1 c.
proof: Proof. unfold lit_insert; intros l1 l2 c; split; intros H. apply insert_inv with (1 := H). case H; intros H1; subst. apply insert_in; auto. exact lit_test_exact. apply insert_incl; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia