fact: Definition refine s1 s2 := length s1 = size * size /\ length s2 = size * size /\ forall p, valid_pos p -> In (get p s1) ref_list -> get p s1 = get p s2.
imports: List UList Permutation Div OrderedList ListOp Lia