proposition: Lemma wf_disjoint_sum : well_founded leA -> well_founded leB -> well_founded Le_AsB.
proof: Proof. intros. unfold well_founded. destruct a as [a| b]. - apply (acc_A_sum a). apply (H a). - apply (acc_B_sum H b). apply (H0 b). Qed.
imports: Relation_Operators