P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p.
intros.
exact
- ([\lambda y. \lambda p.P y p]
- match p with
+ (match p return \lambda y. \lambda p.P y p with
[refl_eq \Rightarrow H]).
qed.
qed.
theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
-simplify.intros.elim H. apply refl_eq.
+unfold symmetric.intros.elim H. apply refl_eq.
qed.
theorem sym_eq : \forall A:Type.\forall x,y:A. x=y \to y=x
\def symmetric_eq.
theorem transitive_eq : \forall A:Type. transitive A (eq A).
-simplify.intros.elim H1.assumption.
+unfold transitive.intros.elim H1.assumption.
qed.
theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y \to y=z \to x=z