proposition: Theorem refine_trans s1 s2 s3 : refine s1 s2 -> refine s2 s3 -> refine s1 s3.
proof: Proof. intros (H, (H1, H2)) (H3, (H4, H5)); split; auto. split; auto. intros; rewrite H2; auto. apply H5; auto. rewrite <- H2; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia