proposition: Lemma valid_set_clause : forall rho s, Valuation.wf rho -> valid rho s -> forall pos c, C.valid rho c -> valid rho (set_clause s pos c).
proof: Proof. unfold valid, get, set_clause. intros rho s Hrho Hs pos c Hc id. destruct (reflect_eqb pos id);subst. case_eq (id <? length s); intro H. unfold get;rewrite PArray.get_set_same; trivial. unfold C.valid;rewrite sort_correct;trivial. generalize (Hs id);rewrite !PArray.get_outofbound, PArray.default_set;trivial. rewrite length_set;trivial. rewrite get_set_other;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring