proposition: Theorem valid_lit_refine: forall l s1 s2, refine s1 s2 -> valid_lit l s2 -> valid_lit l s1.
proof: Proof. intros (p, z) s1 s2 H (H0, (H1, H2)); split; auto. contradict H0. case H; intros _ (_, H3); rewrite <- H3; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia