Describir: Verificación formal del cálculo λSF en Coq