INDUCTIVE DEFINITION Acc () [ A:Set, :A→A→Prop ]
OF ARITY A→Prop
BUILT FROM:
     Acc_intro: ∀x:A.(∀y:A.(R y x)→(Acc A R y))→(Acc A R x)