(*#* [natlike_rec2] is the same as [natlike_rec], but with a different proof, designed
to give a better extracted term. *)
(*#* [natlike_rec2] is the same as [natlike_rec], but with a different proof, designed
to give a better extracted term. *)
inline procedural "cic:/Coq/ZArith/Wf_Z/Efficient_Rec/R_wf.con" "Efficient_Rec__" as definition.
inline procedural "cic:/Coq/ZArith/Wf_Z/natlike_rec2.con" as lemma.
inline procedural "cic:/Coq/ZArith/Wf_Z/Efficient_Rec/R_wf.con" "Efficient_Rec__" as definition.
inline procedural "cic:/Coq/ZArith/Wf_Z/natlike_rec2.con" as lemma.