theorem plus_reg_l: \forall (n,m,p:nat). n + m = n + p \to m = p.
intros. apply plus_reg_l; auto.
qed.
theorem plus_reg_l: \forall (n,m,p:nat). n + m = n + p \to m = p.
intros. apply plus_reg_l; auto.
qed.
cic:/Coq/Init/Logic/eq_ind.con
cic:/Coq/Init/Logic/eq_ind_r.con
cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble/f_equal.con
cic:/Coq/Init/Logic/eq_ind.con
cic:/Coq/Init/Logic/eq_ind_r.con
cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble/f_equal.con