proposition: Lemma subFormulaOr : 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 f1 f2 v s; unfold orH; now rewrite subFormulaImp, subFormulaNot. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)