copilot-theorem-3.1: k-induction for Copilot.
Copilot.Theorem
instantiate :: Proof Universal -> Proof Existential Source #
assume :: PropRef Universal -> Proof a Source #
admit :: Proof a Source #
type Proof a = ProofScheme a () Source #
type PropId = String Source #
data PropRef a Source #
data Universal Source #
data Existential Source #