proposition: Theorem lit_test_exact: forall l1 l2, lit_test l1 l2 = eq -> l1 = l2.
proof: Proof. intros l1 l2; case l1; case l2; simpl; auto. intros p2 z2 p1 z1; case_eq (pos_test p1 p2); intros H; auto. intros; discriminate. intros H1; f_equal; try apply pos_test_exact; auto. apply test_exact; auto. intros; discriminate. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia