fact: Fixpoint interpFormula (value : nat -> U M) (f : Formula L) {struct f} : Prop := match f with | equal t s => interpTerm value t = interpTerm value s | atomic r ts => interpRels _ (rel M r) value ts | impH A B => interpFormula value A -> interpFormula value B | notH A => interpFormula value A -> False | forallH v A => forall x : U M, interpFormula (updateValue value v x) A end.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)