proposition: Lemma acc_B_sum : well_founded leA -> forall x:B, Acc leB x -> Acc Le_AsB (inr A x).
proof: Proof. induction 2. apply Acc_intro; intros y H3. inversion_clear H3; auto with sets. apply acc_A_sum; auto with sets. Qed.
imports: Relation_Operators