proposition: Lemma valid_check_clause cid c : forallb2 (fun i j => i =? j) (S.get s cid) (S.sort_uniq c) -> interp_uf rho c.
proof: Proof. intro H. rewrite <- interp_equiv, <- S.sort_uniq_correct; auto. rewrite <- (interp_check_clause _ _ H). now apply Hs. Qed.
imports: State SMT_terms List Bool PArray Int63