proposition: Theorem well_founded_induction_type : forall P : A -> Type, (forall x : A, (forall y : A, R y x -> P y) -> P x) -> forall a : A, P a.
proof: Proof. Proof. intros; apply (Acc_iter P); auto. Defined.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid