[fjfaase]

For more details about the actual proof, see: 'Blueprint for the Liquid Tensor Experiment'

https://leanprover-community.github.io/liquid/index.html