Function normalise_proof 

pub fn normalise_proof(
    proof: &SProof,
    theorem: &TheoremHead<'_>,
    context: &dyn ProofContext,
) -> Result<Proof>

Normalises a surface proof into a portable plan.

Errors

On steps outside the portable proof model, unknown constructors and self-reference.