(∀m,n. Q m n → Q (↑m) (↑n)) →
∀m,n. Q m n.
#Q #IH1 #IH2 #IH3 #m @(nat_ind_succ … m) -m [ // ]
#m #IH #n @(nat_ind_succ … n) -n /2 width=1 by/
qed-.
(∀m,n. Q m n → Q (↑m) (↑n)) →
∀m,n. Q m n.
#Q #IH1 #IH2 #IH3 #m @(nat_ind_succ … m) -m [ // ]
#m #IH #n @(nat_ind_succ … n) -n /2 width=1 by/
qed-.