proposition: Lemma subNNHelp : forall (f : Formula L) (v : nat) (s : Term L), substF (nnHelp f) v s = nnHelp (substF f v s).
proof: Proof. intro f; elim f using Formula_depth_ind2; intros; try reflexivity. - simpl; rewrite subFormulaImp, H, H0. now rewrite subFormulaImp. - simpl; rewrite subFormulaNot, H, subFormulaNot; easy. - simpl; do 2 rewrite subFormulaForall. simpl; induction (eq_nat_dec v v0). + simpl; reflexivity. + induction (In_dec eq_nat_dec v (freeVarT s)) as [? | ?]. * simpl; repeat rewrite subFormulaNot; repeat rewrite H. -- now rewrite <- freeVarNNHelp. -- eapply eqDepth. ++ symmetry; apply subFormulaDepth. ++ apply depthForall. -- apply depthForall. * repeat rewrite subFormulaNot. rewrite H; simpl. -- reflexivity. -- apply depthForall. Qed.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)