proposition: Lemma wf_symprod : well_founded leA -> well_founded leB -> well_founded Symprod.
proof: Proof. red. destruct a. apply Acc_symprod; auto with sets. Defined.
imports: EqdepFacts Relation_Operators Transitive_Closure Inclusion Inverse_Image