fact: Fixpoint subAllFormula (f : Formula) (m : (nat -> Term)) {struct f} : Formula := match f with | (t = s)%fol => equal (subAllTerm t m) (subAllTerm s m) | atomic r ts => atomic r (subAllTerms _ ts m) | (f -> g)%fol => (subAllFormula f m -> subAllFormula g m)%fol | (~ f)%fol => (~ subAllFormula f m)%fol | (allH n, f)%fol => let nv := newVar (freeVarF f ++ freeVarMap (freeVarF (allH n, f)%fol) m) in (allH nv, (subAllFormula f (fun v : nat => match eq_nat_dec v n with | left _ => var nv | right _ => m v end)))%fol end.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)