proposition: Theorem valid_refine: forall cs s1 s2, refine s1 s2 -> valid cs s2 -> valid cs s1.
proof: Proof. intros cs s1 s2 H H1 n c Hn l Hl. apply valid_lit_refine with (1 := H). apply (H1 n c); auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia