proposition: Lemma subFormulaAnd : forall (f1 f2 : fol.Formula L) (v : nat) (s : fol.Term L), substF (f1 /\ f2)%fol v s = (substF f1 v s /\ substF f2 v s)%fol.
proof: Proof. intros ? ? ? ?; unfold andH in |- *. rewrite subFormulaNot, subFormulaOr; now repeat rewrite subFormulaNot. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)