proposition: Lemma makeTraceNotNice (f2 : fol.Formula L) (z1 z2 : nat * fol.Term L -> nat) : (forall q : nat * fol.Term L, z1 q = z2 q) -> forall q : nat * fol.Term L, makeTraceNot f2 z1 q = makeTraceNot f2 z2 q.
proof: Proof. intros H q; unfold makeTraceNot; now rewrite H. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)