theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
unfold symmetric.intros.elim H. apply refl_eq.
qed.
theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
unfold symmetric.intros.elim H. apply refl_eq.
qed.
\def symmetric_eq.
theorem transitive_eq : \forall A:Type. transitive A (eq A).
unfold transitive.intros.elim H1.assumption.
qed.
\def symmetric_eq.
theorem transitive_eq : \forall A:Type. transitive A (eq A).
unfold transitive.intros.elim H1.assumption.
qed.
cic:/matita/logic/equality/eq_ind.con
cic:/matita/logic/equality/eq_elim_r.con
cic:/matita/logic/equality/eq_f.con
cic:/matita/logic/equality/eq_ind.con
cic:/matita/logic/equality/eq_elim_r.con
cic:/matita/logic/equality/eq_f.con