proposition: Lemma valid_set_weaken : forall rho s, Valuation.wf rho -> valid rho s -> forall pos cid w, valid rho (set_weaken s pos cid w).
proof: Proof. intros. apply S.valid_set_clause_keep; auto. apply check_weaken_valid; auto. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring