proposition: Remark addPairwiseEquals (T : fol.System L) (n : nat) (ts ss : fol.Terms L n): PairwiseEqual T n ts ss -> forall m0 : nat -> fol.Term L, (forall q : nat, q < n + n -> m0 q = termsMap n ts ss q) -> forall f0 : fol.Formula L, SysPrf T (subAllFormula L (nat_rec (fun _ : nat => fol.Formula L) f0 (fun (n : nat) (Hrecn : fol.Formula L) => (v#(n + n) = v#(S (n + n)) -> Hrecn)%fol ) n) m0) -> SysPrf T (subAllFormula L f0 m0).
proof: Proof. intros H. set (m := termsMap n ts ss) in *. induction n as [| n Hrecn]. - simpl in |- *; auto. - simpl in (value of m); simpl in H. destruct (consTerms L n ts) as [[a b] p]. induction (consTerms L n ss) as [[a0 b0] p0]. simpl in H; simpl in (value of m). destruct H as (H, H0); simpl in |- *. intros m0 H1 f0 H2; apply (Hrecn b b0). + auto. + intros q H3; rewrite H1. * unfold m in |- *. destruct (eq_nat_dec q (n + n))as [e | n0]. -- subst; lia. -- induction (eq_nat_dec q (S (n + n))). ++ elim (Compat815.lt_not_le _ _ H3). rewrite a1. apply Nat.le_succ_diag_r. ++ reflexivity. * rewrite Nat.add_succ_r. simpl in |- *. repeat apply Nat.lt_lt_succ_r. auto. + apply (impE L) with (m0 (n + n) = m0 (S (n + n)))%fol. * apply H2. * rewrite Nat.add_succ_r in H1. repeat rewrite H1. unfold m in |- *. destruct (eq_nat_dec (n + n) (n + n)) as [a1 | b1]. -- destruct (eq_nat_dec (S (n + n)) (n + n)) as [e | n0]. ++ lia. ++ induction (eq_nat_dec (S (n + n)) (S (n + n))) as [a2 | b2]. apply H. elim b2; auto. -- elim b1; auto. -- simpl in |- *. lia. -- simpl in |- *; lia. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(ListExt folProp folProof) hydras.Ackermann(subProp folReplace subAll misc) hydras(Compat815)