6 coercion cic:/matita/tests/push_pop_status/cAB.con.
8 inductive eq (A:Type) (x:A) : A \to Prop \def
12 notation "hvbox(a break === b)" non associative with precedence 45 for @{ 'eqqq $a $b }.
13 interpretation "test" 'eqqq x y = (cic:/matita/tests/push_pop_status/eq.ind#xpointer(1/1) _ x y).
16 \forall A. \forall x:A. \forall P: \forall y:A. x===y \to Type.
17 P ? (refl_eq ? x) \to \forall y:A. \forall p:x===y. P y p.
20 (match p1 return \lambda y. \lambda p.P y p with
21 [refl_eq \Rightarrow p]).
24 lemma sym_eq : \forall A:Type.\forall x,y:A. x===y \to y===x.
25 intros.elim H. apply refl_eq.
28 lemma trans_eq : \forall A:Type.\forall x,y,z:A. x===y \to y===z \to x===z.
29 intros.elim H1.assumption.
33 \forall A:Type.\forall x:A. \forall P: A \to Prop.
34 P x \to \forall y:A. y===x \to P y.
35 intros. elim (sym_eq ? ? ? H1).assumption.
39 \forall A:Type.\forall x:A. \forall P: A \to Set.
40 P x \to \forall y:A. y===x \to P y.
41 intros. elim (sym_eq ? ? ? H).assumption.
45 \forall A:Type.\forall x:A. \forall P: A \to Type.
46 P x \to \forall y:A. y===x \to P y.
47 intros. elim (sym_eq ? ? ? H).assumption.
50 theorem eq_f: \forall A,B:Type.\forall f:A\to B.
51 \forall x,y:A. x===y \to f x === f y.
52 intros.elim H.apply refl_eq.
55 theorem eq_f': \forall A,B:Type.\forall f:A\to B.
56 \forall x,y:A. x===y \to f y === f x.
57 intros.elim H.apply refl_eq.
62 cic:/matita/tests/push_pop_status/eq.ind
63 cic:/matita/tests/push_pop_status/sym_eq.con
64 cic:/matita/tests/push_pop_status/trans_eq.con
65 cic:/matita/tests/push_pop_status/eq_ind.con
66 cic:/matita/tests/push_pop_status/eq_elim_r.con
67 cic:/matita/tests/push_pop_status/eq_rec.con
68 cic:/matita/tests/push_pop_status/eq_elim_r'.con
69 cic:/matita/tests/push_pop_status/eq_rect.con
70 cic:/matita/tests/push_pop_status/eq_elim_r''.con
71 cic:/matita/tests/push_pop_status/eq_f.con
72 cic:/matita/tests/push_pop_status/eq_f'.con. (* \x.sym (eq_f x) *)
74 include "push_pop_status_aux1.ma".
75 (* include "push_pop_status_aux2.ma". *)
78 theorem prova: \forall x:A. eq A x x.
83 theorem prova1: \forall x:A. x === x.
84 intros. apply refl_eq.
88 theorem pippo: A -> B.