proposition: Lemma acc_A_B_lexprod : forall x:A, Acc leA x -> (well_founded leB) -> forall y:B, Acc leB y -> Acc lexprod (pair x y).
proof: Proof. induction 1 as [x _ IHAcc]; intros H2 y. induction 1 as [x0 H IHAcc0]. apply Acc_intro. destruct y as [x2 y1]; intro Hlex. depelim Hlex. - apply IHAcc; auto with Relations. - now apply IHAcc0. Defined.
imports: Equations.HoTT.Loader Equations.HoTT.Relation Equations.HoTT.WellFounded HoTT(Spaces.Nat)