default "equality"
cic:/Coq/Init/Logic/eq.ind
cic:/Coq/Init/Logic/sym_eq.con
cic:/Coq/Init/Logic/trans_eq.con
cic:/Coq/Init/Logic/eq_ind.con
cic:/Coq/Init/Logic/eq_ind_r.con
default "equality"
cic:/Coq/Init/Logic/eq.ind
cic:/Coq/Init/Logic/sym_eq.con
cic:/Coq/Init/Logic/trans_eq.con
cic:/Coq/Init/Logic/eq_ind.con
cic:/Coq/Init/Logic/eq_ind_r.con