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. intros; apply Acc_rect; auto. Defined.
imports: Notations Ltac Logic Datatypes