== Para reflexão ==
* Como você procederia para tentar verificar a seguinte igualdade? <math>[\llbracket ![ t [x \mapsto u ] ] \rrbracket!]^{<I,\rho>} = [\llbracket ![ t ]\rrbracket!]^{<I,\rho[x := [[u]]^{<I,\rho>} ]>}</math>
* O que você acha que deve mudar, na interpretação de fórmulas relacionais, no contexto de uma semântica para a ''Lógica de Primeira Ordem Intuicionista''? O que dizer, também, da interpretação de fórmulas quantificadas, nesta lógica? Por fim, como você acha que a relação de ''desigualdade'' poderia ser afetada, no caso intuicionista?
* Como você demonstraria a ''correção'' da regra de congruencialidade do símbolo de igualdade?