proposition: Lemma LNN2LNT_freeVarF (f : fol.Formula LNN) (v : nat): In v (freeVarF (LNN2LNT_formula f)) <-> In v (freeVarF f).
proof: Proof. induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]. - simpl; repeat rewrite LNN2LNT_freeVarT; tauto. - destruct r. simpl. destruct (consTerms _ _ t) as [(a,b) p]. simpl in p; rewrite <- p. destruct (consTerms _ _ b) as [(a0, b0) p0]. simpl in p0; rewrite <- p0. rewrite translateLT1. rewrite <- (nilTerms _ b0). unfold freeVarTs in |- *. fold (@freeVarT LNN) in |- *. rewrite app_nil_r. split. + intros H; decompose record (freeVarSubAllFormula1 _ _ _ _ H) /r. intros H x [H0| H0] H2. * rewrite <- H0 in H2. simpl in H2. rewrite LNN2LNT_freeVarT in H2; auto with datatypes. * destruct H0 as [H0| H0]. -- rewrite <- H0 in H2. simpl in H2. rewrite LNN2LNT_freeVarT in H2. auto with datatypes. -- contradiction. + intro H; destruct (in_app_or _ _ _ H) as [H0 | H0]. * eapply freeVarSubAllFormula2. simpl in |- *. left. reflexivity. simpl in |- *. rewrite LNN2LNT_freeVarT. auto. * eapply freeVarSubAllFormula2. simpl in |- *. right. left. reflexivity. simpl in |- *. rewrite LNN2LNT_freeVarT. auto. - simpl in |- *. induction Hrecf1 as (H, H0). induction Hrecf0 as (H1, H2). split. + intros H3; apply in_or_app. destruct (in_app_or _ _ _ H3); tauto. + intros H3; apply in_or_app. destruct (in_app_or _ _ _ H3); tauto. - assumption. - simpl in |- *. induction Hrecf as (H, H0). split. + intros H1; apply in_in_remove. * eapply in_remove_neq; apply H1. * apply H; eapply List.in_remove; apply H1. + intros H1; apply in_in_remove. * eapply in_remove_neq, H1. * apply H0. eapply in_remove, H1. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)