proposition: Remark substituteFormulaForallNice : forall (v : nat) (a : fol.Formula L) (z1 z2 : forall b : fol.Formula L, lt_depth b (forallH v a) -> nat * fol.Term L -> {y : fol.Formula L | depth L y = depth L b}), (forall (b : fol.Formula L) (q : lt_depth b (forallH v a)) (r : nat * fol.Term L), z1 b q r = z2 b q r) -> forall q : nat * fol.Term L, substituteFormulaForall v a z1 q = substituteFormulaForall v a z2 q.
proof: Proof. intros v a z1 z2 H [a0 b]; unfold substituteFormulaForall in |- *. destruct (eq_nat_dec v a0) as [e | n] ; simpl in |- *. - reflexivity. - induction (In_dec eq_nat_dec v (freeVarT b)); simpl in |- *. + rewrite H; destruct (z2 a (depthForall L a v) (v, var (newVar (a0 :: freeVarT b ++ freeVarF a)))). now rewrite H. + now rewrite H. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)