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