proposition: Theorem invariant_equiv: forall cs s1 s2, refine s1 s2 -> refine s2 s1 -> invariant cs s1 -> invariant cs s2.
proof: Proof. intros cs s1 s2 H1 H2 (H3, (H4, (H5, H6))). split; auto. split; auto. apply valid_refine with (1 := H2); auto. split; auto. case H2; auto. intros s3 H7; split; intros H8. case (H6 s3); auto. apply refine_trans with (1 := H1); auto. case (H6 s3); auto. apply refine_trans with (1 := H1); auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia