proposition: Lemma valid_make : forall rho nclauses, Valuation.wf rho -> valid rho (make nclauses).
proof: Proof. unfold valid, make, get;intros. rewrite PArray.get_make; apply C.interp_true;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring