proposition: Theorem well_founded_induction : forall P:A -> Set, (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
proof: Proof. exact (fun P:A -> Set => well_founded_induction_type P). Defined.
imports: Notations Ltac Logic Datatypes