proposition: Lemma freeVarAddExists2 : forall (n m v : nat) (A : Formula), In v (freeVarF (addExists m n A)) -> n + m <= v \/ v < m.
proof: Proof. intros n m v A H. induction n as [| n Hrecn]; try lia. simpl in H. simpl in |- *. assert (In v (freeVarF (addExists m n A))) as H1. { eapply in_remove. exact H. } pose proof (in_remove _ _ _ _ H). pose proof (Hrecn 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)