-theorem eq_rect':
- \forall A. \forall x:A. \forall P: \forall y:A. x=y \to Type.
- P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p.
- intros.
- exact
- (match p1 return \lambda y. \lambda p.P y p with
- [refl_eq \Rightarrow p]).
-qed.
-
-variant reflexive_eq : \forall A:Type. reflexive A (eq A)
-\def refl_eq.
-
-theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
-unfold symmetric.intros.elim H. apply refl_eq.
-qed.
-
-variant 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).
-unfold transitive.intros.elim H1.assumption.
-qed.
-
-variant trans_eq : \forall A:Type.\forall x,y,z:A. x=y \to y=z \to x=z
-\def transitive_eq.
-
-theorem symmetric_not_eq: \forall A:Type. symmetric A (λx,y.x ≠ y).
-unfold symmetric.simplify.intros.unfold.intro.apply H.apply sym_eq.assumption.
-qed.
-
-variant sym_neq: ∀A:Type.∀x,y.x ≠ y →y ≠ x
-≝ symmetric_not_eq.
-
-theorem eq_elim_r:
- \forall A:Type.\forall x:A. \forall P: A \to Prop.
- P x \to \forall y:A. y=x \to P y.
-intros. elim (sym_eq ? ? ? H1).assumption.
-qed.
-
-theorem eq_elim_r':
- \forall A:Type.\forall x:A. \forall P: A \to Set.
- P x \to \forall y:A. y=x \to P y.
-intros. elim (sym_eq ? ? ? H).assumption.
-qed.
-
-theorem eq_elim_r'':
- \forall A:Type.\forall x:A. \forall P: A \to Type.
- P x \to \forall y:A. y=x \to P y.
-intros. elim (sym_eq ? ? ? H).assumption.
-qed.
-
-theorem eq_f: \forall A,B:Type.\forall f:A\to B.
-\forall x,y:A. x=y \to f x = f y.
-intros.elim H.apply refl_eq.
-qed.
-
-theorem eq_f': \forall A,B:Type.\forall f:A\to B.
-\forall x,y:A. x=y \to f y = f x.
-intros.elim H.apply refl_eq.
-qed.