kdrag.theories.int.induct_nat

kdrag.theories.int.induct_nat(P)