proposition: Lemma substExHC (A : Formula) (v x : nat)(t: Term): v <> x -> ~ In v (freeVarT t) -> substF (existH v A) x t = existH v (substF A x t).
proof: Proof. intro H; rewrite (subFormulaExist). destruct (eq_nat_dec v x) as [H0 | H0]; try congruence. destruct (In_dec eq_nat_dec v (freeVarT t)) as [i | i]; try reflexivity. intro; contradiction. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)