proposition: Lemma subWithEqualsTerms (a b : fol.Term L) (n : nat) (ts : fol.Terms L n) (v : nat) (T : fol.System L): SysPrf T (a = b)%fol -> PairwiseEqual T _ (substTs ts v a) (substTs ts v b).
proof: Proof. intros H; induction ts as [| n t ts Hrects]; simpl in |- *. - auto. - destruct (consTerms L n (Tcons (substT t v a) (substTs ts v a))) as [[a0 b0] p]. destruct (consTerms L n (Tcons (substT t v b) (substTs ts v b))) as [[a1 b1] e]. simpl in |- *; simpl in p, e. inversion p. inversion e. split. + apply subWithEqualsTerm; auto. + rewrite (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H2). now rewrite (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H4). Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(ListExt folProp folProof) hydras.Ackermann(subProp folReplace subAll misc) hydras(Compat815)