@@ -45,7 +45,7 @@ The common logical framework used for all the libraries at our disposal -- name
Hence every application of a function in pvs -- as \mmt-term: $\oma{\cn{pvsapply}}{A,B,f,a}$ -- has two additional implicit arguments, which we eliminate by replacing this expression by $\oma{f}{a}$.
This prevents false negatives due to mismatching type arguments in the presence of subtyping.
\item Since judgments -- in our imports -- correspond to constants of type $\vdash P$ for some proposition $P$, we can use the curry-howard form, we can use the curry-howard correspondence to equate the type $\vdash(P \Rightarrow Q)$ with the function type $(\vdash P)\to(\vdash Q)$, as well as the judgment $\vdash\forall x : A.\;P$ with the function type $(x:A)\to\vdash P$.
\item Since judgments -- in our imports -- correspond to constants of type $\vdash P$ for some proposition $P$, we can use the curry-howard correspondence to equate the type $\vdash(P \Rightarrow Q)$ with the function type $(\vdash P)\to(\vdash Q)$, as well as the judgment $\vdash\forall x : A.\;P$ with the function type $(x:A)\to\vdash P$.
Since both styles of formalization are more or less preferred in different systems, we replace each occurence of the former by the latter.
\item For classical logics, we rewrite all remaining logical connectives using their usual definitions on the basis of negation and conjunction only. Double negations are eliminated.
