proposition: Lemma subFormulaEqual : forall (t1 t2 : fol.Term L) (v : nat) (s : fol.Term L), substF (t1 = t2)%fol v s = (substT t1 v s = substT t2 v s)%fol.
proof: Proof. reflexivity. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)