proposition: Remark subAllnVars1 (a : nat) (ts ss : fol.Terms L a): ts = subAllTerms L _ (fst (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 (fst (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). simpl in H. induction H as [H| H]. rewrite <- H. rewrite Nat.add_succ_r. simpl in |- *. apply Nat.lt_lt_succ_r. apply Nat.lt_succ_diag_r . rewrite Nat.add_succ_r. apply Nat.lt_trans with (a + a). apply Hreca. apply H. simpl in |- *. apply Nat.lt_lt_succ_r. apply Nat.lt_succ_diag_r . } simpl in |- *. induction (consTerms L a ts) as [(a0,b) p]. induction (consTerms L a ss) as [ (a1, b0) p0]. simpl in |- *. simpl in H. induction (nVars L a) as [a2 b1]. simpl in |- *. simpl in Hreca. destruct (eq_nat_dec (a + a) (a + a)) as [e | n]. { simpl in p. rewrite <- p. replace (subAllTerms L a a2 (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 a2 (termsMap a b b0)). + now rewrite <- Hreca. + apply subAllTerms_ext. intros m H0. destruct (eq_nat_dec m (a + a)) as [e0 | n]. * elim (Compat815.lt_not_le m (a + a)). -- apply H; auto. -- lia. * destruct (eq_nat_dec m (S (a + a))) as [a4 | _]. -- elim (Compat815.lt_not_le m (a + a)). apply H; auto. rewrite a4; apply Nat.le_succ_diag_r. -- reflexivity. } + elim n; auto. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(ListExt folProp folProof) hydras.Ackermann(subProp folReplace subAll misc) hydras(Compat815)