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.HoTT.Loader Equations.HoTT.Relation Equations.HoTT.WellFounded HoTT(Spaces.Nat)