proofs.py

def prove_instance(proof, instance):
    """ Return a proof of the given instance of the inference rule that proof
        proves, via the same inference rules used by proof """
    # Task 5.2.1
    instantiation_map = dict()
    if not instance.is_instance_of(proof.statement, instantiation_map):
        return None
    my_lines = []
    for line in proof.lines:
        my_lines.append(
            DeductiveProof.Line(
                instantiate(line.conclusion, instantiation_map),
                line.rule, line.justification)
        )
    return DeductiveProof(instance, proof.rules, my_lines)