proposition: Lemma codeFreeVarListFormulaCorrect (l : list Formula): codeFreeVarListFormula (codeList (map (codeFormula) l)) = codeList (freeVarListFormula L l).
proof: Proof. unfold codeFreeVarListFormula; set (A := fun l0 recs : nat => switchPR l0 (codeApp (codeFreeVarFormula (car (pred l0))) (codeNth (l0 - S (cdr (pred l0))) recs)) 0) in *. induction l as [| a l Hrecl]; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList in |- *; rewrite computeEvalStrongRecHelp; unfold compose2, evalComposeFunc, evalOneParamList, evalList in |- *. - simpl; rewrite cPairProjections1; reflexivity. - unfold A at 1; rewrite evalStrongRecHelp1; simpl. + repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite Hrecl, codeFreeVarFormulaCorrect. apply codeAppCorrect. + apply Compat815.le_lt_n_Sm, cPairLe2A. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(List Arith) hydras.Ackermann(ListExt) hydras(folProp code Compat815)