fact: Fixpoint Acc_intro_generator n (wf : well_founded R) := match n with | O => wf | S n => fun x => Acc_intro x (fun y _ => Acc_intro_generator n (Acc_intro_generator n wf) y) end.
imports: Notations Ltac Logic Datatypes