+Utilizzando il lemma `sem_bool` si ottiene l'ipotesi aggiuntiva
+`([[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1)`. Si procede poi per casi
+su di essa.
+
+1. caso in cui vale `[[ FAtom x ]]_v = 0`.
+
+ Componendo le ipotesi induttive con `[[ FAtom x ]]_v = 0` e
+ espandendo alcune definizioni si ottengono
+ `([[ f[FBot/x ] ]]_v = [[ f ]]_v)` e
+ `([[ f1[FBot/x ] ]]_v = [[ f1 ]]_v)`.
+
+ La sotto prova termina con una catena di uguaglianze che
+ lavora sul lato sinistro della tesi.
+ Espandendo alcune definizioni, utilizzando
+ `[[ FAtom x ]]_v = 0` e le nuove ipotesi appena ottenute
+ si arriva a `(min [[ f ]]_v [[ f1 ]]_v)`.
+ Tale espressione è uguale alla parte destra della conclusione.
+
+1. caso in cui vale `[[ FAtom x ]]_v = 1`.
+
+ Analogo al precedente.
+