1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "static_2/notation/relations/ideq_3.ma".
16 include "static_2/syntax/teqg_ext.ma".
17 include "static_2/syntax/teq.ma".
19 (* SYNTACTIC EQUIVALENCE ****************************************************)
21 definition ceq: relation3 lenv term term ≝
24 definition ceq_ext: lenv → relation bind ≝
28 "context-dependent syntactic equivalence (term)"
29 'IdEq L T1 T2 = (ceq L T1 T2).
32 "context-dependent syntactic equivalence (binder)"
33 'IdEq L I1 I2 = (ceq_ext L I1 I2).
35 (* Basic properties *********************************************************)
37 lemma ceq_ext_refl (L):
38 reflexive … (ceq_ext L).
39 /2 width=1 by ext2_refl/ qed.
41 lemma ceq_ext_sym (L):
42 symmetric … (ceq_ext L).
43 #L @ext2_sym (**) (* full auto does not work *)
44 /2 width=1 by teq_sym/
47 (* Basic inversion lemmas ***************************************************)
49 lemma ceq_ext_inv_eq (L):
50 ∀I1,I2. L ⊢ I1 ≡ I2 → I1 = I2.
52 /3 width=4 by teq_inv_eq, eq_f3/