proposition: Lemma codeCloseCorrect (f : Formula) : codeClose (codeFormula f) = codeFormula (close L f).
proof: Proof. unfold close, codeClose, codeFormula; rewrite codeFreeVarFormulaCorrect, codeNoDupCorrect. apply codeCloseListCorrect. Qed.
imports: Coq(Ensembles List Arith Lia) hydras(primRec cPair folProp code codeList codeFreeVar extEqualNat prLogic codeNatToTerm Compat815)