proposition: Lemma codeNVarsCorrect (n: nat) : codeNVars1 n = codeTerms (fst (nVars L n)) /\ codeNVars2 n = codeTerms (snd (nVars L n)).
proof: Proof. split. - induction n as [| n Hrecn]. + cbn; reflexivity. + simpl; rewrite Hrecn. destruct (nVars L n); simpl; reflexivity. - induction n as [| n Hrecn]. + simpl; reflexivity. + simpl; rewrite Hrecn. destruct (nVars L n); simpl; reflexivity. Qed.
imports: Coq(Arith Lia) hydras.Ackermann(primRec codeFreeVar codeSubFormula cPair code folProp extEqualNat wellFormed folProof prLogic) hydras(Compat815)