Definition istotalnatleh : istotal natleh. Proof. intros x y. induction (isdecrelnatleh x y) as [ lxy | lyx ]. - apply (hinhpr (ii1 lxy)). - apply hinhpr. apply ii2. apply (iscoasymmnatleh _ _ lyx). Defined.