IT/Description/drules.tex

727 \subsection{\texorpdfstring{Specializzazione ($\forall$-eliminazione)}{Specializzazione (per ogni-eliminazione)}}
751 \item $\turn \forall = (\lquant{P}P = (\lquant{x}\T))$ \hfill
752 [\rul{INST\_TYPE} applicata alla definizione di $\forall$]
753 \item $\Gamma\turn \forall(\lquant{x}t)$\hfill [Ipotesi]
805 \subsection{\texorpdfstring{Generalizzazione ($\forall$-introduzione)}{Generalizzazione (per ogni-introduzione)}}%
832 \item $\turn \forall(\lquant{x}t) = \forall(\lquant{x}t)$\hfill [\rul{REFL}]
833 \item $\turn \forall = (\lquant{P} P =(\lquant{x}\T))$\hfill
834 [\rul{INST\_TYPE} applicata alla definizione di $\forall$]
835 \item $\turn\forall(\lquant{x}t)=(\lquant{P} P=(\lquant{x}\T))(\lquant{x}t)$
839 \item $\turn\forall(\lquant{x}t) = ((\lquant{x}t)=(\lquant{x}\T))$
841 \item $\turn((\lquant{x}t)=(\lquant{x}\T)) = \forall(\lquant{x}\T)$
843 \item $\Gamma\turn\forall(\lquant{x}t)$\hfill [\rul{EQ\_MP} 9,3]