proposition: Remark subAllnVars2 (a : nat) (ts ss : fol.Terms L a): ss = subAllTerms L _ (snd (nVars L a)) (termsMap a ts ss).
proof: Proof. induction a as [| a Hreca]. - simpl; symmetry; apply (nilTerms L). - assert (H: forall v : nat, In v (freeVarTs (snd (nVars L a))) -> v < a + a). { intros v H; clear Hreca ss ts; induction a as [| a Hreca]. - elim H. - simpl in H; induction (nVars L a) as [a0 b]. simpl in H; destruct H as [H| H]. subst. lia. rewrite Nat.add_succ_r. simpl in |- *. apply Nat.lt_trans with (a + a). + apply Hreca, H. + lia. } simpl in |- *; destruct (consTerms L a ts) as [[a0 b] e]; destruct (consTerms L a ss) as [[a1 b0] p]. simpl in |- *; simpl in H. induction (nVars L a) as [a2 b1]. Opaque eq_nat_dec. simpl. Transparent eq_nat_dec. destruct (eq_nat_dec (S (a+a)) (a + a)) as [e0 | n]. + lia. + destruct (eq_nat_dec (S (a + a)) (S (a+a))) as [e0 | n0]. * replace (subAllTerms L a b1 (fun n : nat => match eq_nat_dec n (a + a) with | left _ => a0 | right _ => match eq_nat_dec n (S (a + a)) with | left _ => a1 | right _ => termsMap a b b0 n end end)) with (subAllTerms L a b1 (termsMap a b b0)). rewrite <- Hreca; now rewrite <- p. apply subAllTerms_ext. intros m H0. destruct (eq_nat_dec m (a + a)) as [e1 | n1]. -- elim (Compat815.lt_not_le m (a + a)). apply H; auto. rewrite e1; auto. -- destruct (eq_nat_dec m (S (a + a))) as [e1 | n2]. ++ elim (Compat815.lt_not_le m (a + a)). apply H; auto. lia. ++ easy. * elim n0; auto. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(ListExt folProp folProof) hydras.Ackermann(subProp folReplace subAll misc) hydras(Compat815)