[PartiallyTyped]

Taking this a step further, if the AI could write Daphne, it could rely on invariants and pre and post conditions for this proof, no?