proposition: Theorem well_founded_induction_type_2 : (forall (x:A) (x':B), (forall (y:A) (y':B), R (y, y') (x, x') -> P y y') -> P x x') -> forall (a:A) (b:B), P a b.
proof: Proof. intros; apply Fix_F_2; auto. Defined.
imports: Notations Ltac Logic Datatypes