proposition: Theorem sat_refine: forall cs s1 s2, refine s1 s2 -> valid cs s1 -> sat cs s1 -> sat cs s2.
proof: Proof. intros cs s1 s2 H1 H2 H3 n c Hn. case (H3 n c Hn); intros (p, z) (Hl1, Hl2); simpl in Hl2. exists (L p z); split; simpl; auto. case H1; auto. intros H4 (H5, H6); rewrite <- H6; auto. case (H2 n c Hn (L p z) Hl1); intuition. rewrite Hl2; case (H2 n c Hn (L p z) Hl1); intuition. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia