proposition: Lemma translateLT1 : forall a a0 b0, translateLT (Tcons a (Tcons a0 b0)) = subAllFormula LNT LTFormula (fun H : nat => nat_rec (fun _ : nat => fol.Term LNT) (LNN2LNT_term a) (fun (H0 : nat) (_ : fol.Term LNT) => nat_rec (fun _ : nat => fol.Term LNT) (LNN2LNT_term a0) (fun (H1 : nat) (_ : fol.Term LNT) => var H1) H0) H).
proof: Proof. intros a a0 b0; unfold translateLT. destruct (consTerms LNN 1 (Tcons a (Tcons a0 b0))) as [(a1, b) p]. simpl; destruct (consTerms LNN 0 b) as [(a2, b1) p0]. simpl in p; inversion p. assert (b = Tcons a0 b0) by refine (inj_pair2_eq_dec _ eq_nat_dec _ _ _ _ H1). rewrite H in p0; simpl in p0; inversion p0; reflexivity. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)