proposition: Lemma translateProof (U : fol.System LNN) (V : System): ClosedSystem LNT V -> (forall f : fol.Formula LNN, mem (fol.Formula LNN) U f -> SysPrf V (LNN2LNT_formula f)) -> forall f : fol.Formula LNN, folProof.SysPrf LNN U f -> SysPrf V (LNN2LNT_formula f).
proof: Proof. intros H H0 f [x H1]. assert (H2: forall f : fol.Formula LNN, mem (fol.Formula LNN) U f -> exists Axm : Formulas, ex (fun _ : Prf LNT Axm (LNN2LNT_formula f) => forall g : Formula, In g Axm -> mem (fol.Formula LNT) V g) /\ (forall v : nat, In v (freeVarListFormula LNT Axm) -> In v (freeVarF f))). { intros f0 H2; destruct (H0 f0 H2) as [x0 H3]. exists x0; split. - apply H3. - intros v H4; destruct H3. clear x1; induction x0. + elim H4. + destruct (in_app_or _ _ _ H4) as [H5 | H5]. * elim H with v a. apply H3. auto with *. assumption. * apply IHx0. firstorder. apply H5. } destruct H1. destruct (translatePrf U V H2 f x x0 H1). exists x1; tauto. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)