proposition: Remark makeTrace1 (f : fol.Formula L) (v : nat) (s : fol.Term L): cTriplePi1 (makeTrace f (v, s)) = cTriple v (codeTerm s) (codeFormula f).
proof: Proof. induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]; unfold makeTrace, makeTraceImp, makeTraceNot, Formula_depth_rec2, Formula_depth_rec in |- *; simpl in |- *; try (rewrite cTripleProj1; reflexivity). unfold makeTraceForall; destruct (eq_nat_dec n (fst (v, s))) as [a| b]; simpl. - rewrite cTripleProj1; reflexivity. - destruct (In_dec eq_nat_dec n (freeVarT s)); simpl; rewrite cTripleProj1; reflexivity. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)