fact: Definition codeClose (f : nat) : nat := codeCloseList (codeNoDup (codeFreeVarFormula f)) f.
imports: Coq(Ensembles List Arith Lia) hydras(primRec cPair folProp code codeList codeFreeVar extEqualNat prLogic codeNatToTerm Compat815)