proposition: Lemma subAddExistsNice : forall (n m : nat) (A : Formula) (v : nat) (s : Term), n + m <= v \/ v < m -> (forall v : nat, In v (freeVarT s) -> n + m <= v \/ v < m) -> substF (addExists m n A) v s = addExists m n (substF A v s).
proof: Proof. intros n m A v s H H0. induction n as [| n Hrecn]; simpl in |- *; auto. rewrite (subFormulaExist LNN). destruct (eq_nat_dec (n + m) v) as [e | e]; try lia. destruct (in_dec Nat.eq_dec (n + m) (freeVarT s)) as [e0 | e0]. - pose proof (H0 _ e0). lia. - rewrite Hrecn. + reflexivity. + lia. + intros v0 H1. pose proof (H0 _ H1). lia. Qed.
imports: Coq(Arith) hydras.Ackermann(extEqualNat subAll folProp subProp folReplace folLogic3 NN NNtheory primRec expressible) Coqprime(ChineseRem) Coq(Vector List Lia) hydras(ListExt cPair MoreDecidable) hydras(Compat815 ssrnat_extracts) Coq(Utf8)