proposition: Lemma equalRelation (T : fol.System L) (r : Relations L) (ts ss : fol.Terms L _): PairwiseEqual T _ ts ss -> SysPrf T (atomic r ts <-> atomic r ss)%fol.
proof: Proof. intros H. set (n := arityR L r) in *. set (m := termsMap n ts ss) in *. rewrite (subAllnVars1 _ ts ss). fold m in |- *; rewrite (subAllnVars2 _ ts ss); fold m in |- *. replace (iffH (atomic r (subAllTerms L n (fst (nVars L n)) m)) (atomic r (subAllTerms L n (snd (nVars L n)) m))) with (subAllFormula L (iffH (atomic r (fst (nVars L n))) (atomic r (snd (nVars L n)))) m); [ idtac | reflexivity ]. cut (SysPrf T (subAllFormula L (AxmEq4 L r) m)). - unfold AxmEq4 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 => iffH (atomic r a) (atomic r b)) (nVars L n)) with (iffH (atomic r (fst (nVars L n))) (atomic r (snd (nVars L n)))). + generalize (iffH (atomic r (fst (nVars L n))) (atomic r (snd (nVars L n)))). intros f H0; apply (addPairwiseEquals T n ts ss). * auto. * unfold m in |- *; auto. * auto. + destruct (nVars L n) as [a b]. reflexivity. - replace (subAllFormula L (AxmEq4 L r) m) with (subAllFormula L (AxmEq4 L r) (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)). intros f H0; destruct H0. clear m H ts ss T. induction n as [| n Hrecn]. * simpl in |- *; exists (nil (A:=fol.Formula L)). exists (EQ4 L r); 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]. destruct (consTerms L n ss) as [[a b0] p0]. simpl in |- *. induction (eq_nat_dec m0 (n + n)) as [a1 | b1]. ** subst; lia. ** destruct (eq_nat_dec m0 (S (n + n))). 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)