Deduzione naturale con quantificatore universale

[erika09091]

Buona domenica a tutti, ho un problema su un esercizio di logica matematica riguardo la deduzione naturale. Devo svolgere il seguente esercizio:
$AA$x A(x) $vv$ $AA$x B(x) |- $AA$x (A(x) $vv$ B(x))

io ho fatto nel seguente modo:

1 $AA$x A(x) $vv$ $AA$x B(x) premessa
2* $AA$x A(x) assunzione
3* A(c) $AA$-eliminazione(2)
4* A(c) $vv$ B(x) $vv$-introduzione(3)
5* $AA$x (A(x) $vv$ B(x)) $AA$-introduzione(4)
6 $AA$x A(x) $=>$ $AA$x (A(x) $vv$ B(x)) $=>$-introduzione(2,5)
7* $AA$x B(x) assunzione
8* B(c) $AA$-eliminazione(7)
9* A(x) $vv$ B(c) $vv$-introduzione(8)
10* $AA$x (A(x) $vv$ B(x)) $AA$-introduzione(9)
11 $AA$x B(x) $=>$ $AA$x (A(x) $vv$ B(x)) $=>$-introduzione(7,10)
12 $AA$x (A(x) $vv$ B(x)) regola derivata (1, 6, 11)

ma è corretto? dal punto 4 in cui ho un A(c) $vv$ B(x) posso dedurre il punto 5?

grazie per le eventuali risposte

[el_brando]

A me sembra di sì.
In teoria lo puoi fare perchè $ c $ e $ x $ non compaiono libere nelle ipotesi che hanno generato $ A(c) vv B(x) $...

[erika09091]

ah ok grazie mille