Defesa de Dissertação de Mestrado: Using LEAN to show that every exponentially big normal proof in Minimal Implicational Logic is exponentially redundant