proposition: Lemma makeTraceForallNice (v0 : nat) (a : fol.Formula L) (z1 z2 : forall b : fol.Formula L, lt_depth L b (forallH v0 a) -> nat * fol.Term L -> nat): (forall (b : fol.Formula L) (q : lt_depth L b (forallH v0 a)) (r : nat * fol.Term L), z1 b q r = z2 b q r) -> forall q : nat * fol.Term L, makeTraceForall v0 a z1 q = makeTraceForall v0 a z2 q.
proof: Proof. intros H q; unfold makeTraceForall; now repeat rewrite H. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)