Introducción al curso y al cálculo proposicional en Coq