proposition: Theorem wf_lexprod : well_founded leA -> well_founded leB -> well_founded lexprod.
proof: Proof. intros wfA wfB; unfold well_founded. destruct x. apply acc_A_B_lexprod; auto with relations; intros. Defined.
imports: Equations.Type.Loader Equations.Type.Relation Equations.Type.WellFounded