proposition: Lemma subFormulaExist : forall (f : fol.Formula L) (x v : nat) (s : fol.Term L), let nv := newVar (v :: freeVarT s ++ freeVarF f) in substF (existH x f) v s = match eq_nat_dec x v with | left _ => existH x f | right _ => match In_dec eq_nat_dec x (freeVarT s) with | right _ => existH x (substF f v s) | left _ => existH nv (substF (substF f x (var nv)) v s) end end.
proof: Proof. intros ? ? ? ? nv; unfold existH. rewrite subFormulaNot, subFormulaForall. destruct (eq_nat_dec x v). - reflexivity. - induction (In_dec eq_nat_dec x (freeVarT s)); now repeat rewrite subFormulaNot. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)