proposition: Lemma subWithEqualsTerm (a b t : fol.Term L) (v : nat) (T : fol.System L): SysPrf T (a = b)%fol -> SysPrf T (substT t v a = substT t v b)%fol.
proof: Proof. intros H; elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => PairwiseEqual T _ (substTs ts v a) (substTs ts v b)); simpl in |- *. - intros n; induction (eq_nat_dec v n); [easy | apply eqRefl]. - intros f t0 H0; apply equalFunction. apply H0. - auto. - intros. destruct (consTerms L n (Tcons (substT t0 v a) (substTs t1 v a))). destruct x as [a0 b0]. destruct (consTerms L n (Tcons (substT t0 v b) (substTs t1 v b))). destruct x as [a1 b1]. simpl in |- *. simpl in e0; simpl in e. inversion e0. inversion e. auto. rewrite (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H4). rewrite (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H6). auto. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(ListExt folProp folProof) hydras.Ackermann(subProp folReplace subAll misc) hydras(Compat815)