DISP	valuation_df	(<F:Formula:L> under <a:Assignment:L>) == (<F> under <a>)
ABS	valuation	(F under a) == (letrec val f = case f: x (a x); p val p; pq val p val q; pq val p val q; pq val p val q; ) F
ML	valuation_unroll	let get_formula_type_from_valuation = fst o fst o dest_term o snd o hd o snd o dest_term ;; let valuationC t = FwdMacroC (concat `valuation_` (concat (get_formula_type_from_valuation t) `_unrollC`)) (AllC [UnfoldC `valuation`; letrec_unrollC; formula_case_unrollC; TryC (FoldC `valuation`)]) t ;; let valuation_unrollC = FirstC (map valuationC [(x under a) ; (P under a) ; (PQ under a) ; (PQ under a) ; (PQ under a) ]) ;; add_AbReduce_conv `valuation` valuation_unrollC;;
THM	valuation_wf	a:Assignment. F:Formula. (F under a)

the other theories