fact: Fixpoint LNN2LNT_term (t : fol.Term LNN) : fol.Term LNT:= match t with | var v => var v | apply f ts => apply LNT f (LNN2LNT_terms _ ts) end with LNN2LNT_terms (n : nat) (ts : fol.Terms LNN n) {struct ts} : Terms n := match ts in (fol.Terms _ n0) return (Terms n0) with | Tnil => @Tnil LNT | Tcons m s ss => Tcons (LNN2LNT_term s) (LNN2LNT_terms m ss) end.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)