proposition: Lemma codeCloseListCorrect (l : list nat) (f : Formula): codeCloseList (codeList l) (codeFormula f) = codeFormula (closeList L l f).
proof: Proof. set (g := fun l recs f : nat => switchPR l (cPair 3 (cPair (car (pred l)) (codeNth (l - S (cdr (pred l))) recs))) f). induction l as [| a l Hrecl]. - simpl; unfold codeCloseList, evalStrongRec in |- *; simpl. rewrite cPairProjections1; reflexivity. - simpl; unfold codeCloseList; fold g. assert (H :forall n m : nat, m < n -> extEqual 1 (evalComposeFunc 1 1 (Vector.cons _ (evalStrongRecHelp 1 g n) 0 (Vector.nil _)) (fun b : nat => codeNth (n - S m) b)) (evalStrongRec 1 g m)). { intros n m H; apply (evalStrongRecHelp2 1); assumption. } simpl in H; unfold evalStrongRec in |- *. unfold evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList in |- *. unfold g at 1; rewrite H. + simpl; repeat rewrite cPairProjections1 || rewrite cPairProjections2. rewrite <- Hrecl; reflexivity. + simpl; apply Compat815.le_lt_n_Sm, cPairLe2A. Qed.
imports: Coq(Ensembles List Arith Lia) hydras(primRec cPair folProp code codeList codeFreeVar extEqualNat prLogic codeNatToTerm Compat815)