proposition: Lemma reduceAddExistsOneWay : forall (n m : nat) (A B : Formula), SysPrf NN (impH A B) -> SysPrf NN (impH (addExists m n A) (addExists m n B)).
proof: Proof. intros n m A B H. apply impI. induction n as [| n Hrecn]. - apply impE with A. + apply sysWeaken. apply H. + apply Axm; right; constructor. - simpl in |- *. apply existSys. + apply closedNN. + simpl in |- *; intro H0. destruct (in_remove _ _ _ _ H0). congruence. + apply existSimp. exact Hrecn. 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)