set ::= [] | N :: set

X in [] = False
X in N::L = X=N \/ X in L

Theorem: forall Z, not (Z in \emptyset)
 assumo Z numero naturale
 dimostro Z in \emptyset => False (P)
  assumo Z in \emptyset
  o equivalentemente Z in []
  o equivalentemente False (H)
  per H ovvio
 per P concludo not (Z in \emptyset)
ovvio.

[] union L2 = L2
H::L union L2 = H::(L union L2)

Teorema: per ogni L1,L2,Z.
 Z in (L1 union L2) => Z in L1 \/ Z in L2
 assumo L1 set
 per induzione su L1 dimostro
  per ogni L2,Z. Z in (L1 union L2) => Z in L1 \/ Z in L2
 
 caso []:
  debbo dimostrare
   per ogni L2,Z. Z in ([] union L2) => Z in [] \/ Z in L2
  o equivalentemente
   per ogni L2,Z. Z in L2 => False \/ Z in L2
    assumo L2 set
    assumo Z numero naturale
    suppongo Z in L2 (H)
     per H ovvio

 caso N::L:
  per ipotesi induttiva
   per ogni L2,Z. Z in (L union L2) => Z in L \/ Z in L2
  debbo dimostrare
  per ogni L2,Z. Z in (N::L union L2)=> Z in N::L \/ Z in L2
  o equivalentemente
   per ogni L2,Z. Z in N::(L union L2) =>
    Z=N \/ Z in L \/ Z in L2
  o equivalentemente
   per ogni L2,Z. Z=N \/ Z in (L union L2) =>
    Z=N \/ Z in L \/ Z in L2
  assumo L2 set
  assumo Z numero naturale
  suppongo Z=N \/ Z in (L union L2) (K)
   procedo per casi
     caso Z=N:
      debbo dimostrare Z=N \/ Z in L \/ Z in L2
      per ipotesi, ovvio

     caso Z in (L union L2):
      debbo dimostrare Z=N \/ Z in L \/ Z in L2
      dall'ipotesi, con l'ipotesi induttiva, concludo
       Z in L \/ Z in L2
      quindi ovvio
qed.

Teorema: per ogni L1,L2,Z.
  Z in L1 \/ Z in L2 => Z in (L1 union L2)
per induzione strutturale su L1 dimostro
 per ogni L2,Z. Z in L1 \/ Z in L2 => Z in (L1 union L2)

caso []:
 debbo dimostrare
   per ogni L2,Z. Z in [] \/ Z in L2 => Z in ([] union L2)
 o equivalentemente
   per ogni L2,Z. False \/ Z in L2 => Z in L2
   assume L2 set
   assume Z natural number
   suppose False \/ Z in L2.
   procedo per casi
     caso False (H):
      ovvio perchè ho raggiunto l'assurdo

     caso Z in L2 (H):
      ovvio per H

caso N::L:
 per ipotesi induttiva
  per ogni L2,Z. Z in L \/ Z in L2 => Z in (L union L2)
 debbo dimostrare
  per ogni L2,Z. Z in N::L \/ Z in L2=> Z in (N::L union L2)
 o equivalentemente
  per ogni L2,Z. Z=N \/ Z in L \/ Z in L2
    => Z in N::(L union L2)
 o equivalentemente
  per ogni L2,Z. Z=N \/ Z in L \/ Z in L2
    => Z=N \/ Z in (L union L2)
  assumo L2 set
  assumo Z numero naturale
  suppongo Z=N \/ Z in L \/ Z in L2
  procedo per casi:

    caso Z=N (H):
      ovvio per H

    caso Z in L \/ Z in L2 (H):
      debbo dimostrare Z=N \/ Z in (L union L2)
      per H, ipotesi induttiva
    ovvio
qed.