kdrag.kernel.induct_inductive

kdrag.kernel.induct_inductive(x: DatatypeRef, P: QuantifierRef) → Proof

Build a basic induction principle for an algebraic datatype

Parameters:

• x (DatatypeRef)

• P (QuantifierRef)

Return type:

Proof