proposition: Lemma equalFunction (T : fol.System L) (f : Functions L) (ts ss : fol.Terms L _): PairwiseEqual T _ ts ss -> SysPrf T (apply f ts = apply f ss)%fol.
proof: Proof. intros H. set (n := arityF L f) in *. set (m := termsMap n ts ss) in *. rewrite (subAllnVars1 _ ts ss). fold m in |- *. rewrite (subAllnVars2 _ ts ss). fold m in |- *. replace (equal (apply f (subAllTerms L n (fst (nVars L n)) m)) (apply f (subAllTerms L n (snd (nVars L n)) m))) with (subAllFormula L (equal (apply f (fst (nVars L n))) (apply f (snd (nVars L n)))) m); [ idtac | reflexivity ]. cut (SysPrf T (subAllFormula L (AxmEq5 L f) m)). - unfold AxmEq5 in |- *; fold n in |- *. replace (prod_rec (fun _ : fol.Terms L n * fol.Terms L n => fol.Formula L) (fun a b : fol.Terms L n => equal (apply f a) (apply f b)) (nVars L n)) with (equal (apply f (fst (nVars L n))) (apply f (snd (nVars L n)))). + generalize (equal (apply f (fst (nVars L n))) (apply f (snd (nVars L n)))). intros f0 H0; apply (addPairwiseEquals T n ts ss). auto. unfold m in |- *; auto. auto. + induction (nVars L n) as [a b]. reflexivity. - replace (subAllFormula L (AxmEq5 L f) m) with (subAllFormula L (AxmEq5 L f) (fun x : nat => match le_lt_dec (n + n) x with | left _ => var x | right _ => m x end)). + apply (subAllCloseFrom L). apply sysExtend with (Empty_set (fol.Formula L)). red; destruct 1. clear m H ts ss T; induction n as [| n Hrecn]. * simpl in |- *. exists (nil (A:=fol.Formula L)). exists (EQ5 L f). contradiction. * simpl in |- *; apply (forallI L). apply (notInFreeVarSys L). rewrite Nat.add_succ_r. simpl in |- *. apply (forallI L). apply (notInFreeVarSys L). apply Hrecn. + apply subAllFormula_ext. intros m0 H0; clear H0 H. destruct (le_lt_dec (n + n) m0) as [l | l]. * unfold m in |- *. induction n as [| n Hrecn]. -- reflexivity. -- simpl in |- *. destruct (consTerms L n ts) as [(a0, b) p]. induction (consTerms L n ss) as [(a1, b0) p0]. simpl in |- *. induction (eq_nat_dec m0 (n + n)). ++ lia. ++ induction (eq_nat_dec m0 (S (n + n))). subst; lia. apply Hrecn. lia. * reflexivity. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(ListExt folProp folProof) hydras.Ackermann(subProp folReplace subAll misc) hydras(Compat815)